Formal Techniques in Real-Time and Fault-Tolerant Systems: Third International Symposium Organized Jointly with the Working Group Provably Correct Sys (Paperback, 1994)

Hybrid verification by exploiting the environment.- Correctness of real time systems by construction.- Specifying and verifying fault-tolerant systems.- Development of hybrid systems.- Linear duration invariants.- Efficient reconfiguration of trees: A case study in methodical design of nonmasking fault-tolerant programs.- A comparison of Statecharts variants.- A calculus of stochastic systems.- Verification of an audio control protocol.- Verifying invariance properties of timed systems with duration variables.- Predicting logical and temporal properties of real-time systems using Synchronized Elementary Nets.- Designing and implementing correct real-time systems.- Specification and refinement of finite dataflow networks - a relational approach.- Activation-oriented specification of real-time systems.- Provably Correct Systems.- Simulation approach to provably correct hardware compilation.- Verification methods for the divergent runs of clock systems.- Fault-tolerant bisimulation and process transformations.- Layering of real-time distributed processes.- Testing and refinement for nondeterministic and probabilistic processes.- Proving safety properties of hybrid systems.- A layered real-time specification of a RISC processor.- A real time fault tolerant microprocessor based On-Board Computer System for INSAT-2 spacecraft.- Reasoning about durations in Metric Temporal Logic.- Scheduling in critical real-time systems: a manifesto.- Stepwise development of fault-tolerant reactive systems.- Distributed implementation of SIGNAL: Scheduling & graph clustering.- Derivation of the input conditional formula from a reactive system specification in temporal logic.- From physical modelling to compositional models of hybrid systems.- Specification and transformation of reactive systems with time restrictions and concurrency.- Languages for reactive specifications: Synchrony vs asynchrony.- Specification and verification of controlled systems.- Towards a duration calculus proof assistant in PVS.- Algebraic reasoning for real-time probabilistic processes with uncertain information.- Specifying timed state sequences in powerful decidable logics and timed automata.- A calculus for hybrid sampled data systems.- Formal design of hybrid systems.- A formal proof of the Deadline Driven scheduler.- Tools Demonstration.