Formal Modeling and Analysis of Timed Systems: First International Workshop, FORMATS 2003, Marseille, France, September 6-7, 2003, Revised Papers (Lecture Notes in Computer Science (2791))

This book constitutes the thoroughly refereed post-proceedings of the First International Workshop on Formal Modeling and Analysis of Timed Systems, FORMATS 2003, held in Marseille, France in September 2003. The 19 revised full papers presented together with an invited paper and the abstracts of two invited talks were carefully selected from 36 submissions during two rounds of reviewing and improvement. All current aspects of formal method for modeling and analyzing timed systems are addressed; among the timed systems dealt with are timed automata, timed Petri nets, max-plus algebras, real-time systems, discrete time systems, timed languages, and real-time operating systems. Front Matter....Pages - Timed Automata and Timed Languages Challenges and Open Problems....Pages 1-1 Towards Efficient Partition Refinement for Checking Reachability in Timed Automata....Pages 2-17 Checking ACTL * Properties of Discrete Timed Automata via Bounded Model Checking....Pages 18-33 Removing Irrelevant Atomic Formulas for Checking Timed Automata Efficiently....Pages 34-45 Adding Symmetry Reduction to Uppaal ....Pages 46-59 TIMES: A Tool for Schedulability Analysis and Code Generation of Real-Time Systems....Pages 60-72 Optimization of Timed Automata Models Using Mixed-Integer Programming....Pages 73-87 Discrete-Time Rewards Model-Checked....Pages 88-104 Performance Analysis of Probabilistic Timed Automata Using Digital Clocks....Pages 105-120 An Interval-Based Algebra for Restricted Event Detection....Pages 121-133 PARS: A Process Algebra with Resources and Schedulers....Pages 134-150 Formal Semantics of Hybrid Chi....Pages 151-165 Run-Time Guarantees for Real-Time Systems....Pages 166-167 A Nonarchimedian Discretization for Timed Languages....Pages 168-181 Folk Theorems on the Determinization and Minimization of Timed Automata....Pages 182-188 Control Synthesis for a Smart Card Personalization System Using Symbolic Model Checking....Pages 189-203 On Timing Analysis of Combinational Circuits....Pages 204-218 Analysis of Real Time Operating System Based Applications....Pages 219-233 Time-Optimal Test Cases for Real-Time Systems....Pages 234-245 Using Zone Graph Method for Computing the State Space of a Time Petri Net....Pages 246-259 Causal Time Calculus....Pages 260-272 ELSE : A New Symbolic State Generator for Timed Automata....Pages 273-280 Back Matter....Pages - Formal Modeling and Analysis of Timed Systems: First International Workshop, FORMATS 2003, Marseille, France, September 6-7, 2003. Revised Papers Author: Kim Guldstrand Larsen, Peter Niebert Published by Springer Berlin Heidelberg ISBN: 978-3-540-21671-1 DOI: 10.1007/b12025 Table of Contents: Timed Automata and Timed Languages Challenges and Open Problems Towards Efficient Partition Refinement for Checking Reachability in Timed Automata Checking ACTL Removing Irrelevant Atomic Formulas for Checking Timed Automata Efficiently Adding Symmetry Reduction to Uppaal TIMES: A Tool for Schedulability Analysis and Code Generation of Real-Time Systems Optimization of Timed Automata Models Using Mixed-Integer Programming Discrete-Time Rewards Model-Checked Performance Analysis of Probabilistic Timed Automata Using Digital Clocks An Interval-Based Algebra for Restricted Event Detection PARS: A Process Algebra with Resources and Schedulers Formal Semantics of Hybrid Chi Run-Time Guarantees for Real-Time Systems A Nonarchimedian Discretization for Timed Languages Folk Theorems on the Determinization and Minimization of Timed Automata Control Synthesis for a Smart Card Personalization System Using Symbolic Model Checking On Timing Analysis of Combinational Circuits Analysis of Real Time Operating System Based Applications Time-Optimal Test Cases for Real-Time Systems Using Zone Graph Method for Computing the State Space of a Time Petri Net

This book constitutes the thoroughly refereed post-proceedings of the First International Workshop on Formal Modeling and Analysis of Timed Systems, FORMATS 2003, held in Marseille, France in September 2003.

The 19 revised full papers presented together with an invited paper and the abstracts of two invited talks were carefully selected from 36 submissions during two rounds of reviewing and improvement. All current aspects of formal method for modeling and analyzing timed systems are addressed; among the timed systems dealt with are timed automata, timed Petri nets, max-plus algebras, real-time systems, discrete time systems, timed languages, and real-time operating systems.

Model checking is an approach commonly applied for automated verification of reachability properties.