This volume contains the proceedings of FTRTFT 2002, the International S- posium on Formal Techniques in Real-Time and Fault-Tolerant Systems, held at the University of Oldenburg, Germany, 9–12 September 2002. This sym- sium was the seventh in a series of FTRTFT symposia devoted to problems and solutions in safe system design. The previous symposia took place in Warwick 1990, Nijmegen 1992, Lub ¨ eck 1994, Uppsala 1996, Lyngby 1998, and Pune 2000. Proceedings of these symposia were published as volumes 331, 571, 863, 1135, 1486, and 1926 in the LNCS series by Springer-Verlag. This year the sym- sium was co-sponsored by IFIP Working Group 2.2 on Formal Description of Programming Concepts. The symposium presented advances in the development and use of formal techniques in the design of real-time, hybrid, fault-tolerant embedded systems, covering all stages from requirements analysis to hardware and/or software - plementation. Particular emphasis was placed on UML-based development of real-time systems. Through invited presentations, links between the dependable systems and formal methods research communities were strengthened. With the increasing use of such formal techniques in industrial settings, the conference aimed at stimulating cross-fertilization between challenges in industrial usages of formal methods and advanced research. Inresponsetothecallforpapers,39submissionswerereceived.Eachsubm- sion was reviewed by four program committee members assisted by additional referees. At the end of the reviewing process, the program committee accepted 17 papers for presentation at the symposium.
Author(s): Gerd Behrmann, Johan Bengtsson, Alexandre David, Kim G. Larsen, Paul Pettersson (auth.), Werner Damm, Ernst -Rüdiger Olderog (eds.)
Series: Lecture Notes in Computer Science 2469
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2002
Language: English
Pages: 462
Tags: Programming Languages, Compilers, Interpreters; Logics and Meanings of Programs; Processor Architectures; Special Purpose and Application-Based Systems; Memory Structures; Control Structures and Microprogramming
UppaaL Implementation Secrets....Pages 3-22
Software Hazard and Safety Analysis....Pages 23-34
Real-Time Operating Systems: Problems and Novel Solutions....Pages 37-51
Real-Time UML....Pages 53-70
Eager Class Initialization for Java....Pages 71-80
Applications of Formal Methods in Biology....Pages 81-81
An Overview of Formal Verification for the Time-Triggered Architecture....Pages 83-105
Scheduler Modeling Based on the Controller Synthesis Paradigm....Pages 107-107
Component-Based Synthesis of Dependable Embedded Software....Pages 111-128
From the Specification to the Scheduling of Time-Dependent Systems....Pages 129-145
On Control with Bounded Computational Resources....Pages 147-162
Decidability of Safety Properties of Timed Multiset Rewriting....Pages 165-183
Extending Timed Automaton and Real-Time Logic to Many-Valued Reasoning....Pages 185-204
Fault Diagnosis for Timed Automata....Pages 205-221
Verification of Timed Automata via Satisfiability Checking....Pages 225-243
Take It NP-Easy: Bounded Model Construction for Duration Calculus....Pages 245-264
Towards Bounded Model Checking for the Universal Fragment of TCTL....Pages 265-288
A Typed Interrupt Calculus....Pages 291-310
Parametric Verification of a Group Membership Algorithm....Pages 311-330
A Method for Testing the Conformance of Real Time Systems....Pages 331-351
A Probabilistic Extension of UML Statecharts....Pages 355-374
Eliminating Queues from RT UML Model Representations....Pages 375-393
Model Checking Timed UML State Machines and Collaborations....Pages 395-414
Partial Order Path Technique for Checking Parallel Timed Automata....Pages 417-432
Constructing Test Automata from Graphical Real-Time Requirements....Pages 433-453
