This book constitutes the refereed proceedings of the 5th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT'98, held in Lyngby, Denmark, in September 1998.
The 22 revised full papers presented were carefully selected and reviewed for inclusion in the book. Also included are four invited contributions and five tool demonstrations. The papers address the current aspects of the hot topic of embedded systems, in particular temporal logic, requirements engineering, analysis techniques, verification, model checking, and applications.
Author(s): John C. Knight (auth.), Anders P. Ravn, Hans Rischel (eds.)
Series: Lecture Notes in Computer Science 1486
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 1998
Language: English
Pages: 347
Tags: Programming Languages, Compilers, Interpreters; Logics and Meanings of Programs; Processor Architectures; Special Purpose and Application-Based Systems; Operating Systems
Challenges in the utilization of formal methods....Pages 1-17
On the need for practical formal methods....Pages 18-26
A general framework for the composition of timed systems....Pages 27-28
Operational and logical semantics for polling real-time systems....Pages 29-40
A finite-domain semantics for testing temporal logic specifications....Pages 41-54
Duration Calculus of Weakly Monotonic Time....Pages 55-64
Reuse in requirements engineering: Discovery and application of a real-time requirement pattern....Pages 65-74
A modular visual model for hybrid systems....Pages 75-91
Integrating real-time structured design and formal techniques....Pages 92-102
Duration Calculus in the specification of safety requirements....Pages 103-112
Automated stream-based analysis of fault-tolerance....Pages 113-122
Designing a provably correct robt control system using a ‘lean’ formal method....Pages 123-132
Static analysis to identify invariants in RSML specifications....Pages 133-142
Partition refinement in real-time model checking....Pages 143-157
Formal verification of stabilizing systems....Pages 158-172
Synchronizing clocked transition systems....Pages 173-185
Some decidability results for duration calculus under synchronous interpretation....Pages 186-197
Fair synchronous transition systems and their liveness proofs....Pages 198-209
Dynamical properties of timed automata....Pages 210-227
An algorithm for the approximative analysis of rectangular automata....Pages 228-240
On checking parallel real-time systems for linear duration properties....Pages 241-250
A practical and complete algorithm for testing real-time systems....Pages 251-261
Mechanical verification of clock synchronization algorithms....Pages 262-271
Compiling graphical real-time specifications into silicon....Pages 272-281
Towards a formal semantics of verilog using duration calculus....Pages 282-293
The ICOS synthesis environment....Pages 294-297
Kronos: A model-checking tool for real-time systems....Pages 298-302
SGLOT: A visual tool for structural LOTOS specifications....Pages 303-306
Discrete-time Promela and Spin....Pages 307-310
Moby/PLC — Graphical development of PLC-automata....Pages 311-314
Predictability in critical systems....Pages 315-338
