This volume presents the proceedings of the Third International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems held jointly with the Working Group Provably Correct Systems (ProCoS) at Lübeck, Germany in September 1994.
The book contains full versions of 5 invited talks and 33 carefully selected refereed contributions as well as 12 tool demonstrations. It documents that formal techniques constitute the foundation of a systematic design of real-time, fault-tolerant, and hybrid systems, throughout the whole engineering process, from the capture of requirements through specification, design, coding and compilation, right down to the hardware that embeds the system into its environment.
Author(s): Limor Fix, Fred B. Schneider (auth.), Hans Langmaack, Willem-Paul de Roever, Jan Vytopil (eds.)
Series: Lecture Notes in Computer Science 863
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 1994
Language: English
Pages: 787
Tags: Programming Languages, Compilers, Interpreters; Logics and Meanings of Programs; Processor Architectures; Special Purpose and Application-Based Systems; Memory Structures; Control Structures and Microprogramming
Hybrid verification by exploiting the environment....Pages 1-18
Correctness of real time systems by construction....Pages 19-40
Specifying and verifying fault-tolerant systems....Pages 41-76
Development of hybrid systems....Pages 77-85
Linear duration invariants....Pages 86-109
Efficient reconfiguration of trees: A case study in methodical design of nonmasking fault-tolerant programs....Pages 110-127
A comparison of Statecharts variants....Pages 128-148
A calculus of stochastic systems....Pages 149-169
Verification of an audio control protocol....Pages 170-192
Verifying invariance properties of timed systems with duration variables....Pages 193-210
Predicting logical and temporal properties of real-time systems using Synchronized Elementary Nets....Pages 211-227
Designing and implementing correct real-time systems....Pages 228-246
Specification and refinement of finite dataflow networks — a relational approach....Pages 247-267
Activation-oriented specification of real-time systems....Pages 268-287
Provably Correct Systems....Pages 288-335
Simulation approach to provably correct hardware compilation....Pages 336-350
Verification methods for the divergent runs of clock systems....Pages 351-372
Fault-tolerant bisimulation and process transformations....Pages 373-392
Layering of real-time distributed processes....Pages 393-417
Testing and refinement for nondeterministic and probabilistic processes....Pages 418-430
Proving safety properties of hybrid systems....Pages 431-454
A layered real-time specification of a RISC processor....Pages 455-475
A real time fault tolerant microprocessor based On-Board Computer System for INSAT-2 spacecraft....Pages 476-487
Reasoning about durations in Metric Temporal Logic....Pages 488-510
Scheduling in critical real-time systems: a manifesto....Pages 511-528
Stepwise development of fault-tolerant reactive systems....Pages 529-546
Distributed implementation of SIGNAL: Scheduling & graph clustering....Pages 547-566
Derivation of the input conditional formula from a reactive system specification in temporal logic....Pages 567-582
From physical modelling to compositional models of hybrid systems....Pages 583-604
Specification and transformation of reactive systems with time restrictions and concurrency....Pages 605-620
Languages for reactive specifications: Synchrony vs asynchrony....Pages 621-640
Specification and verification of controlled systems....Pages 641-659
Towards a duration calculus proof assistant in PVS....Pages 660-679
Algebraic reasoning for real-time probabilistic processes with uncertain information....Pages 680-693
Specifying timed state sequences in powerful decidable logics and timed automata....Pages 694-715
A calculus for hybrid sampled data systems....Pages 716-737
Formal design of hybrid systems....Pages 738-755
A formal proof of the Deadline Driven scheduler....Pages 756-775
Tools Demonstration....Pages 776-787
