Formal Modeling and Analysis of Timed Systems
9th International Conference, FORMATS 2011, Aalborg, Denmark, September 21-23, 2011, Proceedings
Published on 25. September 2011
XI, 353 pages
978-3-642-24310-3 (ISBN)
Description
This book constitutes the refereed proceedings of the 9th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2011, held in Aalborg, Denmark, in September 2011. The 20 revised full papers presented together with three invited talks were carefully reviewed and selected from 43 submissions. The papers are organized in topical sections on probabilistic methods, robustness, games, verification and testing, verification, hybrid systems, and applications.
More details
Other editions
Additional editions
Uli Fahrenberg | Stavros Tripakis
Formal Modeling and Analysis of Timed Systems
9th International Conference, FORMATS 2011, Aalborg, Denmark, September 21-23, 2011, Proceedings
Book
09/2011
1st Edition
Springer
€53.49
Shipment within 7-9 days
Content
- Title
- Preface
- Organization
- Table of Contents
- Invited Talks
- Performance Evaluation of Schedulers in a Probabilistic Setting
- Introduction
- Preliminaries
- Computing Volumes
- Conflicts and Schedulers
- Concluding Remarks
- References
- Formal Modeling and Analysis of Timed Systems: Technology Push or Market Pull?
- Background
- Key Question Addressed
- Observations from the Academic Field
- Observations and Trends in Industry
- Analysis
- Opportunities!
- Epilogue
- References
- Interfaces for Control Components
- References
- Session 1: Probabilistic Models
- Time-Bounded Verification of CTMCs against Real-Time Specifications
- Introduction
- Preliminaries
- Continuous-Time Markov Chains
- Metric Temporal Logic
- Timed Automata
- A Bound on the Number of Discrete Jumps
- MTL Specifications
- Constraints Generation
- Computing Probabilities
- Main Algorithm and Correctness
- TA Specifications
- Constraints Generation
- Algorithm for TA
- Conclusion
- References
- Performance Model Checking Scenario-Aware Dataflow
- Introduction
- Scenario-Aware Dataflow
- TPS Semantics
- Semantic Properties of SADF
- Performance Model Checking
- Strategy for Computing Performance
- Example Performance Metrics
- Metric Dependent State-Space Reduction
- Practical Implementation
- Experimental Results
- Conclusions and Outlook
- References
- Probabilistic Real-Time Rewrite Theories and Their Expressive Power
- Introduction
- Preliminaries
- Probabilistic Real-Time Rewrite Theories
- Example: A Simple Round Trip Time Protocol
- Reachability Probabilities in PRTRTs
- The Expressive Power of PRTRTs
- Probabilistic Timed Automata
- Stochastic Automata
- Deterministic and Stochastic Petri Nets
- Handling Uncertainty in Probabilistic Transitions
- Concluding Remarks
- References
- Statistical Model Checking for Networks of Priced Timed Automata
- Introduction
- Network of Priced Timed Automata
- Probabilistic Semantics of NPTA
- Statistical Model Checking for NPTA
- Beyond ``Classical'' Statistical Model-Checking
- Case Studies
- References
- Session 2: Robustness
- Robust Model-Checking of Timed Automata via Pumping in Channel Machines
- Introduction
- Preliminaries
- Timed Automata
- Robust Model-Checking of Timed Automata
- Results
- Encoding by Channel Machines
- Channel Machine Associated to a Timed Automaton
- Relation with Timed Automata
- -Distance in CA(N)
- Proof
- Proof of the Main Theorem
- Pumping Lemma: Bounded Case
- Making Exact Paths
- Pumping Lemma with Progress Cycles: Unbounded case
- Pumping Lemma with Non-progress Cycles
- References
- Thin and Thick Timed Regular Languages
- Introduction
- Preliminaries
- Timed Languages and Their Measures
- Timed Automata and Their Languages
- Thinness, Simplices and Examples
- More on Paths and Cycles
- Region Graph and State Split Automata
- Paths and Polytopes
- Point to Point Reachability: Algebraic Characterization
- The Thin-Thick Alternative and Its Consequences
- Forgetful Cycles, and the Others
- Pumping Lemma for Long Thick Paths
- Characterizing Thick Languages
- Thin and Thick SCC
- Entropies of Thick Languages
- Conclusion and Future Work
- References
- Robust Specification of Real Time Components
- Introduction
- Background on Timed I/O Specifications
- Robust Timed I/O Specifications
- Robust Consistency and Conjunction
- Robust Compatibility, Composition and Quotient
- Concluding Remarks
- References
- Session 3: Games
- Minimum Attention Controller Synthesis for Omega-Regular Objectives
- Introduction
- Preliminaries
- Imperfect Information Games
- From Imperfect-Information to Perfect-Information
- Minimum Attention Control
- Infinite State Systems
- Discussions
- References
- Crossing the Bridge between Similar Games
- Introduction
- Basics
- Running Example
- Similarity
- Determining Similarity
- Preservation of Logical Properties
- Summary
- References
- Session 4: Verification and Testing
- Exact Incremental Analysis of Timed Automata with an SMT-Solver
- Introduction
- Timed Automata
- Syntax, Semantics, Runs
- Three Decision Problems on TA and DTA
- Bounded Decision Problems
- Incremental Encodings of Some Decision Problems
- A Generic Constraint Logic
- The Incremental Encoding
- Translations into Other Formalisms
- Implementation and Experimental Results
- Further Work
- References
- Segmented State Space Traversal for Conformance Testing of Cyber-Physical Systems
- Introduction
- Background Theory
- Preliminaries
- Quantitative Conformance Testing
- Scalability, an Open Issue
- Segmented State Space Traversal
- Concept and Definitions
- The Procedure
- Case Study
- Summary
- References
- Event Clock Automata: From Theory to Practice
- Introduction
- Preliminaries
- Equivalence Relations for Event-Clocks
- Regions and Event Clocks
- Zones and Event-Clocks
- Future Work: Widening Operators
- References
- On Construction of Safety Signal Automata for MITL[U, S] Using Temporal Projections
- Introduction
- Syntax and Semantics of MTL
- Temporal Projections and S Operator Elimination
- Eliminating Future Modality I
- Eliminating Bounded Future over Infinite signals
- Signal Automata
- MITL to Signal Automata
- Complexity
- References
- Session 5: Verification
- Craig Interpolation in the Presence of Non-linear Constraints
- Introduction
- Foundations
- Basics on iSAT
- Proof Certificates in iSAT
- Construction of Craig Interpolants Using iSAT
- iSAT and BMC with Craig Interpolation
- Basics
- Experiments with iSAT
- Conclusion
- References
- On the Verification of Timed Ad Hoc Networks
- Introduction
- Preliminaries
- Timed Ad Hoc Networks
- Timed Networks
- Undecidability with Dense Time
- Decidability with Dense Time
- Decidability with Discrete Time
- Conclusions
- References
- Session 6: Hybrid Systems
- Incremental Computation of Succinct Abstractions for Hybrid Systems
- Introduction
- Hybrid Systems
- Incremental Abstract Forward/Backward Computation
- Improvements
- Exit Regions
- Avoiding Redundant Edge Checks
- Incremental Refinement of Abstraction
- Implementation
- Widening
- Computation of Reachability Information
- Computational Experiments
- Conclusion
- References
- Composing Stability Proofs for Hybrid Systems
- Introduction
- Motivation
- Preliminaries
- Complexity Reduction for Stability Proof
- Compute Effective Representation of Snapshot Sequences
- Conclusion
- References
- Rigorous Discretization of Hybrid Systems Using Process Calculi
- Introduction
- Syntax
- Semantics
- Behavioral Congruence
- Syntactic Discretization
- Toy Example
- Related Work and Future Work
- References
- Session 7: Applications
- Model-Based Dependability Analysis of Programmable Drug Infusion Pumps
- Introduction
- Motivation
- Preliminaries
- Dependability Analysis
- System Models
- Pump Model
- Patient Model
- Human Interaction Models
- Modeling Operator Mistakes
- Mistake Models
- Analysis Framework
- Experiments
- Related Work and Conclusions
- References
- A Design-for-Verification Framework for a Configurable Performance-Critical Communication Interface
- Introduction
- Related Work
- Common Communication Protocols' Features
- Approaches to Hardware Support of Configurability
- Formal Modelling: Theory, Concepts and Tools
- Tock-CSP
- Abstractions and Refinements and Equivalences
- Formal Modelling: The CSP Models
- The Protocol Abstract Specification
- The Communication Interface Model
- Evaluation
- Basic Functional and Timing Verification
- Instruction-Level Functional Verification
- System-Level Functional Verification
- System-Level Performance Verification
- Protocol Conformance Verification
- Conclusion and Outlook
- References
- Author Index
