Formal Modeling and Analysis of Timed Systems

1. Front Matter

   PDF

2. Interdisciplinary Foundations for Open Cyber-Physical Systems

   • Tarek Abdelzaher

   Pages 1-1

3. Safraless Procedures for Timed Specifications

   • Barbara Di Giampaolo, Gilles Geeraerts, Jean-François Raskin, Nathalie Sznajder

   Pages 2-22

4. Property-Based Monitoring of Analog and Mixed-Signal Systems

   • John Havlicek, Scott Little, Oded Maler, Dejan Nickovic

   Pages 23-24

5. A Framework for Verification of Software with Time and Probabilities

   • Marta Kwiatkowska, Gethin Norman, David Parker

   Pages 25-45

6. Synchrony and Time in Fault-Tolerant Distributed Algorithms

   • Ulrich Schmid

   Pages 46-46

7. Reconciling Urgency and Variable Abstraction in a Hybrid Compositional Setting

   • D. A. van Beek, P. J. L. Cuijpers, J. Markovski, D. E. Nadales Agut, J. E. Rooda

   Pages 47-61

8. Computing Equilibria in Two-Player Timed Games via Turn-Based Finite Games

   • Patricia Bouyer, Romain Brenguier, Nicolas Markey

   Pages 62-76

9. Natural Domain SMT: A Preliminary Assessment

   • Scott Cotton

   Pages 77-91

10. Robust Satisfaction of Temporal Logic over Real-Valued Signals

    • Alexandre Donzé, Oded Maler

    Pages 92-106

11. Combining Symbolic Representations for Solving Timed Games

    • Rüdiger Ehlers, Robert Mattmüller, Hans-Jörg Peter

    Pages 107-121

12. Expected Reachability-Time Games

    • Vojtěch Forejt, Marta Kwiatkowska, Gethin Norman, Ashutosh Trivedi

    Pages 122-136

13. Diagnosis Using Unfoldings of Parametric Time Petri Nets

    • Bartosz Grabiec, Louis-Marie Traonouez, Claude Jard, Didier Lime, Olivier H. Roux

    Pages 137-151

14. From Mtl to Deterministic Timed Automata

    • Dejan Ničković, Nir Piterman

    Pages 152-167

15. Unambiguity in Timed Regular Languages: Automata and Logics

    • Paritosh K. Pandya, Simoni S. Shah

    Pages 168-182

16. A Process Algebraic Framework for Modeling Resource Demand and Supply

    • Anna Philippou, Insup Lee, Oleg Sokolsky, Jin-Young Choi

    Pages 183-197

17. Memory Event Clocks

    • James Jerson Ortiz, Axel Legay, Pierre-Yves Schobbens

    Pages 198-212

18. Simulation and Bisimulation for Probabilistic Timed Automata

    • Jeremy Sproston, Angelo Troina

    Pages 213-227

19. Layered Composition for Timed Automata

    • Ernst-Rüdiger Olderog, Mani Swaminathan

    Pages 228-242

20. A Conformance Testing Relation for Symbolic Timed Automata

    • Sabrina von Styp, Henrik Bohnenkamp, Julien Schmaltz

    Pages 243-255

This volume contains the papers that were presented at the 8th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2010), held September 8–10, 2010, at IST (Institute of Science and Technology) Austria, in Klosterneuburg, Austria. The modeling andanalysis oftiming aspects of systems is a keyproblem that has been treated independently in several di?erent communities in computer science and related areas. Researchers interested in semantics, veri?cation, re- timescheduling,andperformanceanalysisstudymodelssuchastimedautomata and timed Petri nets, the digital design community focuses on propagation and switching delays, and designers of embedded controllers need to take into - count the time requiredby controllersto compute their responses after sampling the environment. Although the timing-related questions in these separate c- munities have their own speci?c nature, there is a growing awareness that there are basic problems that are common to all of them. In particular, all of these disciplines model and analyze systems whose behavior depends on combinations of logical and timing constraints between occurrences of events. The aim of FORMATS is to promote the study of fundamental and practical aspects of timed systems, and to bring together researchers from di?erent d- ciplines that share an interest in the modeling and analysis of timed systems. Typical topics include (but are not limited to): – Foundations and Semantics: theoretical foundations of timed systems and languages; comparison between di?erent models (timed automata, timed Petri nets, hybrid automata, timed process algebra,max-plus algebra, pr- abilistic models).

• Natural
• Simulation
• algorithms
• constraint solving
• data structures
• hardware circuits
• max-plus algebra
• model checking
• modeling
• real-time logistics
• runtime verification
• timed Petri nets
• timed automata
• timed systems
• verification

• Institute of Science and Technology, IST Austria, Klosterneuburg, Austria

  Krishnendu Chatterjee, Thomas A. Henzinger

Policies and ethics