Formal Techniques in Real-Time and Fault-Tolerant Systems

Challenges in the utilization of formal methods.- On the need for practical formal methods.- A general framework for the composition of timed systems.- Operational and logical semantics for polling real-time systems.- A finite-domain semantics for testing temporal logic specifications.- Duration Calculus of Weakly Monotonic Time.- Reuse in requirements engineering: Discovery and application of a real-time requirement pattern.- A modular visual model for hybrid systems.- Integrating real-time structured design and formal techniques.- Duration Calculus in the specification of safety requirements.- Automated stream-based analysis of fault-tolerance.- Designing a provably correct robt control system using a ‘lean’ formal method.- Static analysis to identify invariants in RSML specifications.- Partition refinement in real-time model checking.- Formal verification of stabilizing systems.- Synchronizing clocked transition systems.- Some decidability results for duration calculus under synchronous interpretation.- Fair synchronous transition systems and their liveness proofs.- Dynamical properties of timed automata.- An algorithm for the approximative analysis of rectangular automata.- On checking parallel real-time systems for linear duration properties.- A practical and complete algorithm for testing real-time systems.- Mechanical verification of clock synchronization algorithms.- Compiling graphical real-time specifications into silicon.- Towards a formal semantics of verilog using duration calculus.- The ICOS synthesis environment.- Kronos: A model-checking tool for real-time systems.- SGLOT: A visual tool for structural LOTOS specifications.- Discrete-time Promela and Spin.- Moby/PLC — Graphical development of PLC-automata.- Predictability in critical systems.