This volume constitutes the refereed proceedings of the Fourth International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFTS '96, held in Uppsala, Sweden, in September 1996.
The 22 revised full papers presented were selected from a total of 61 submissions; also included are three invited contributions and five tools demonstrations. The papers are organized in sections on state charts, timed automata, duration calculus, case studies, scheduling, fault tolerance, specification, and verification.
Author(s): Flaviu Cristian (auth.), Bengt Jonsson, Joachim Parrow (eds.)
Series: Lecture Notes in Computer Science 1135
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 1996
Language: English
Pages: 490
Tags: Programming Languages, Compilers, Interpreters; Operating Systems; Logics and Meanings of Programs; Special Purpose and Application-Based Systems; Processor Architectures; Memory Structures
On the semantics of group communication....Pages 1-21
Unifying verification paradigms....Pages 22-39
Formal methods for early fault detection....Pages 40-54
Retiming techniques for Statecharts....Pages 55-71
Compiling Argos into Boolean equations....Pages 72-89
Real-time mode-machines....Pages 90-109
A calculus for timed automata....Pages 110-129
Minimizable timed automata....Pages 130-147
Weak chop inverses and liveness in Mean-Value Calculus....Pages 148-167
Synthesizing controllers from Duration Calculus....Pages 168-187
Sampling semantics of Duration Calculus....Pages 188-207
The production cell: A verified real-time system....Pages 208-227
Verification-driven development of a collision-avoidance protocol for the Ethernet....Pages 228-245
Exhaustive computation of the scheduled task execution sequences of a real-time application....Pages 246-262
Scheduling Data Flow programs in Hard Real-Time environments....Pages 263-278
Dynamic scheduling in the presence of faults: Specification and verification....Pages 279-297
Efficient broadcasting on faulty star networks....Pages 298-305
Model checking for extended timed temporal logics....Pages 306-326
Partial orders and verification of real-time systems....Pages 327-346
Toward a modal theory of types for the π-calculus....Pages 347-365
Graphical formalization of real-time requirements....Pages 366-384
On specifying real-time systems in a causality-based setting....Pages 385-404
Verification of embedded systems using synchronous observers....Pages 405-419
Compositionality in real-time shared variable concurrency....Pages 420-439
Formal analysis of a real-time kernel specification....Pages 440-458
Mona: Decidable arithmetic in practice....Pages 459-462
Verifying synchronous reactive systems programmed in ESTEREL....Pages 463-466
AutoFocus — A tool for distributed systems specification....Pages 467-470
A tool for translation of VHDL descriptions into a formal model and its application to formal verification and synthesis....Pages 471-474
EVGC: A tool for visualizing LOTOS behavioural specifications....Pages 475-478
