Formal Modeling and Analysis of Timed Systems

Name: Formal Modeling and Analysis of Timed Systems | 9th International Conference, FORMATS 2011, Aalborg, Denmark, September 21-23, 2011, Proceedings
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

9th International Conference, FORMATS 2011, Aalborg, Denmark, September 21-23, 2011, Proceedings

Uli Fahrenberg Stavros Tripakis(Herausgeber*in)

Springer (Verlag)

Erschienen am 25. September 2011

XI, 353 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-642-24310-3 (ISBN)

53,49 €inkl. 7% MwSt.

Systemvoraussetzungen

für PDF mit Wasserzeichen-DRM

E-Book Einzellizenz

Als Download verfügbar

Beschreibung

Weitere Details

Weitere Ausgaben

Inhalt

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

Inhalt (PDF)

Systemvoraussetzungen

Als PDF speichern Als Link merken