Formal Modeling and Analysis of Timed Systems: 8th International Conference, FORMATS 2010, Klosterneuburg, Austria, September 8-10, 2010, Proceedings (Lecture Notes in Computer Science (6246))

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). Front Matter....Pages - Interdisciplinary Foundations for Open Cyber-Physical Systems....Pages 1-1 Safraless Procedures for Timed Specifications....Pages 2-22 Property-Based Monitoring of Analog and Mixed-Signal Systems....Pages 23-24 A Framework for Verification of Software with Time and Probabilities....Pages 25-45 Synchrony and Time in Fault-Tolerant Distributed Algorithms....Pages 46-46 Reconciling Urgency and Variable Abstraction in a Hybrid Compositional Setting....Pages 47-61 Computing Equilibria in Two-Player Timed Games via Turn-Based Finite Games....Pages 62-76 Natural Domain SMT: A Preliminary Assessment....Pages 77-91 Robust Satisfaction of Temporal Logic over Real-Valued Signals....Pages 92-106 Combining Symbolic Representations for Solving Timed Games....Pages 107-121 Expected Reachability-Time Games....Pages 122-136 Diagnosis Using Unfoldings of Parametric Time Petri Nets....Pages 137-151 From Mtl to Deterministic Timed Automata....Pages 152-167 Unambiguity in Timed Regular Languages: Automata and Logics....Pages 168-182 A Process Algebraic Framework for Modeling Resource Demand and Supply....Pages 183-197 Memory Event Clocks....Pages 198-212 Simulation and Bisimulation for Probabilistic Timed Automata....Pages 213-227 Layered Composition for Timed Automata....Pages 228-242 A Conformance Testing Relation for Symbolic Timed Automata....Pages 243-255 Back Matter....Pages - Annotation This book constitutes the proceedings of the 8th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2010, held in Klosterneuburg, Austria in September 2010. The 14 papers presented were carefully reviewed and selected from 31 submissions. In addition, the volume contains 3 invited talks and 2 invited tutorials. The aim of FORMATS is to promote the study of fundamental and practical aspects of timed systems, and to bring together researchers from different disciplines that share an interest in the modeling and analysis of timed systems. Typical topics include foundations and semantics, methods and tools, and applications