Formal Modeling and Analysis of Timed Systems
Subtitle: First International Workshop, FORMATS 2003, Marseille, France, September 6-7, 2003, Revised Papers (Lecture Notes in Computer Science)
Contributors: Kim G. Larsen (Editor); Peter Niebert (Editor)
Edition: 1 edition
Publisher: Springer
Published: June 24, 2004
Language: eng
Format: Paperback
Number of pages: 281
ISBN-13: 9783540216711
Subjects: Applied mathematics; Programming - Software Development; Computers - General Information; Computers; Computer Books: General; Programming - Systems Analysis & Design; Data Processing - General; Logic Design; Computers / Logic Design; Programming Languages - General
First sentence: Model checking is an approach commonly applied for automated verification of reachability properties.
Description: Formal Modeling and Analysis of Timed Systems: First International Workshop, FORMATS 2003, Marseille, France, September 6-7, 2003. Revised Papers<br />Author: Kim Guldstrand Larsen, Peter Niebert<br /> Published by Springer Berlin Heidelberg<br /> ISBN: 978-3-540-21671-1<br /> DOI: 10.1007/b12025<br /><br />Table of Contents:<p></p><ul><li>Timed Automata and Timed Languages Challenges and Open Problems
</li><li>Towards Efficient Partition Refinement for Checking Reachability in Timed Automata
</li><li>Checking ACTL
</li><li>Removing Irrelevant Atomic Formulas for Checking Timed Automata Efficiently
</li><li>Adding Symmetry Reduction to Uppaal
</li><li>TIMES: A Tool for Schedulability Analysis and Code Generation of Real-Time Systems
</li><li>Optimization of Timed Automata Models Using Mixed-Integer Programming
</li><li>Discrete-Time Rewards Model-Checked
</li><li>Performance Analysis of Probabilistic Timed Automata Using Digital Clocks
</li><li>An Interval-Based Algebra for Restricted Event Detection
</li><li>PARS: A Process Algebra with Resources and Schedulers
</li><li>Formal Semantics of Hybrid Chi
</li><li>Run-Time Guarantees for Real-Time Systems
</li><li>A Nonarchimedian Discretization for Timed Languages
</li><li>Folk Theorems on the Determinization and Minimization of Timed Automata
</li><li>Control Synthesis for a Smart Card Personalization System Using Symbolic Model Checking
</li><li>On Timing Analysis of Combinational Circuits
</li><li>Analysis of Real Time Operating System Based Applications
</li><li>Time-Optimal Test Cases for Real-Time Systems
</li><li>Using Zone Graph Method for Computing the State Space of a Time Petri Net</li></ul>