Formal Modeling and Analysis of Timed Systems

Name: Formal Modeling and Analysis of Timed Systems | 13th International Conference, FORMATS 2015, Madrid, Spain, September 2-4, 2015, Proceedings
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

13th International Conference, FORMATS 2015, Madrid, Spain, September 2-4, 2015, Proceedings

Sriram Sankaranarayanan Enrico Vicario(Editor)

Springer (Publisher)

Published on 21. August 2015

X, 321 pages

E-Book

PDF with digital watermarking

System requirements

978-3-319-22975-1 (ISBN)

€53.49incl. 7% vat

System requirements

for PDF with digital watermarking

E-Book Single Licence

Available for download

Description

More details

Other editions

Content

Intro
Preface
Organization
Contents
Verification and Control of Probabilistic Rectangular Hybrid Automata
1 Background and Motivation
2 Probabilistic Rectangular Hybrid Automata
3 Approximation with Probabilistic Hybrid Automata
References
Performance Evaluation of an Emergency Call Center: Tropical Polynomial Systems Applied to Timed Petri Nets
1 Introduction
2 A Simplified Petri Net Model of an Emergency Call Center
3 Piecewise Linear Dynamics of Timed Petri Nets with Free Choice and Priority Routing
3.1 Timed Petri Nets: Notation and Semantics
3.2 Timed Petri Nets with Free Choice and Priority Routing
3.3 Piecewise Linear Representation by Counter Variables
4 Computing Stationary Regimes
5 Application to the Emergency Call Center
6 Experiments
7 Concluding Remarks
References
Language Preservation Problems in Parametric Timed Automata
1 Introduction
2 Definitions
3 Undecidability of the Preservation Problems in General
3.1 Undecidability of the Language Preservation Problem
3.2 Undecidability of the Trace Preservation Problem.
3.3 Undecidability of the Robust Language-Preservation Problem
3.4 Undecidability of the Robust Trace Preservation Problem
4 A Semi-algorithm for the Trace Preservation Synthesis
5 Decidability Results for Subclasses of PTA
5.1 1-Clock PTA
5.2 Decidability and Synthesis for Deterministic 1-Clock PTA
5.3 Undecidability for L/U-PTA
5.4 A Decidability Result for 1-Parameter L-PTA and U-PTA
6 Conclusion and Perspectives
References
Timed Symbolic Dynamics
1 Introduction
2 Preliminaries
2.1 Dynamical Systems
2.2 -Entropies and Topological Entropy
2.3 Shift Spaces on General Alphabet
2.4 Edge and Sofic Shifts from Classical Symbolic Dynamics
2.5 Comparison with Finite State Automata
3 Factor Based Characterisations
3.1 Factor Based Characterisation of General Alphabet Shift Spaces
3.2 Entropies for General Alphabet Shift Spaces
3.3 Sliding Block Codes for General Alphabet Shift Spaces
4 Timed Shift Spaces and Their Measures
4.1 Timed Shift Spaces
4.2 Discretisation of Shift Spaces and Their Entropy
4.3 Metric Mean Dimension of Timed Sofic Shifts
5 Conclusion and Perspectives
References
Timed-Automata Abstraction of Switched Dynamical Systems Using Control Funnels
1 Introduction
2 Graphs of Control Funnels
2.1 Control Funnels
2.2 Motion Planning
2.3 Motion Planning with Graphs of Control Funnels
3 Reduction to Timed Automata
4 LQR Funnels
5 Examples of Application
5.1 Synchronization of Sine Waves
5.2 A 1D Pick-and-Place Problem
6 Conclusion and Future Work
References
Quantitative Analysis of Communication Scenarios
1 Introduction
2 Preliminaries
2.1 Branching-Time Models and Quantitative Annotations
2.2 Scenarios Specifying Communication Systems
3 Branching-Time Semantics
3.1 Model Checking Branching-Time Requirements
4 Quantitative Message Sequence Graphs
4.1 Model Checking Quantitative Requirements
5 Implementation and Case Study
5.1 Models and Requirements in our Case Study
5.2 Evaluation
6 Conclusion
References
Multi-objective Parameter Synthesis in Probabilistic Hybrid Systems
1 Introduction
2 Parametric Probabilistic Hybrid Automata
2.1 Interpretation as Parametric Infinite-State Markov Chain
2.2 Parameter Synthesis
3 Estimating Expectations by Sampling
4 Symbolic Representation of Importance Sampling
5 Existence or Absence of Parameter Instances
6 Experiments
7 Related Work
8 Conclusion
References
On the Scalability of Constraint Solving for Static/Off-Line Real-Time Scheduling
1 Introduction
2 Related Work
3 ILP/SMT/CP Modeling of Scheduling Problems
3.1 Single-Period Dependent Tasks, Heterogenous Architecture
3.2 Simplified Encoding for the Homogenous Case
3.3 Multi-period, Non-preemptive, Non-dependent Tasks
3.4 Multi-period, Preemptive, Non-dependent Tasks
4 Test Cases
4.1 Test Case Generation
4.2 Signal Processing Case Studies
5 Experimental Results
5.1 Synthetic Test Cases
5.2 Signal Processing Case Studies
6 Conclusion
References
Improving Search Order for Reachability Testing in Timed Automata
1 Introduction
2 Preliminaries
2.1 Timed Automata and the Reachability Problem
2.2 Symbolic Semantics
2.3 Reachability Algorithm
3 Ranking System
4 Waiting Strategy
4.1 Topological-Like Ordering for a Timed Automaton
4.2 Topological-Like Ordering for Networks of Timed Automata
5 Experimental Evaluation
6 Conclusion
References
Symbolic Minimum Expected Time Controller Synthesis for Probabilistic Timed Automata
1 Introduction
2 Background
3 Probabilistic Timed Automata
4 Minimum Expected Time Algorithm for PTAs
5 Conclusion
References
Quantitative Attack Tree Analysis via Priced Timed Automata
1 Introduction
2 Graphical Security Modeling
2.1 Attack Trees
2.2 Metrics on ATs
3 Priced Timed Automata
4 Analyzing Attack Trees via Price Timed Automata
4.1 From Attack Trees to Price Timed Automata
4.2 Quantitative Analysis of Attack Trees
5 Case Studies
6 Conclusion
References
Fluid Model Checking of Timed Properties
1 Introduction
2 Background and Modelling Language
2.1 Timed Properties
3 Fluid Model Checking of Timed Properties
3.1 The Mean Behaviour of the Population Model
4 Experimental Results
5 Conclusions
References
Nested Timed Automata with Frozen Clocks
1 Introduction
2 Dense Timed Pushdown Automata with Frozen Ages
2.1 Dense Timed Pushdown Automata
2.2 DTPDAs with Frozen Ages
3 Reachability of DTPDAs with Frozen Ages
3.1 Digiword and Its Operations
3.2 Snapshot Pushdown System
3.3 Well-Formed Constraint
4 Nested Timed Automata with Frozen Clocks
4.1 Nested Timed Automata with Frozen Clocks
4.2 Reachability of NeTA-Fs with Multiple Global Clocks
4.3 Reachability of NeTA-F with a Single Global Clock
5 Conclusion
References
Quantitative Analysis of Concurrent Reversible Computations
1 Introduction
2 Continuous-Time Markov Chains
3 Stochastic Automata
4 Reversible Stochastic Automata
4.1 Synchronisation of an Arbitrary Number of Automata
5 Conclusion
References
Hybrid Tools for Hybrid Systems -- Proving Stability and Safety at Once
1 Introduction
2 Related Work
3 Preliminaries
3.1 Checking Stability via Stabhyli
3.2 Checking Reachability via SoapBox
4 Hybrid Stability and Reachability Tool
4.1 Single-Mode Lyapunov Function Computation
4.2 SafeSet Computation
4.3 SafeBox Conversion
4.4 Unrolling Algorithm
4.5 Global Lyapunov Function Computation
5 Benchmarking
6 Summary
References
Verification and Control of Partially Observable Probabilistic Real-Time Systems
1 Introduction
2 Partially Observable Markov Decision Processes
3 Partially Observable Probabilistic Timed Automata
4 Verification and Strategy Synthesis for POPTAs
5 Implementation and Case Studies
6 Conclusions
References
Deciding Concurrent Planar Monotonic Linear Hybrid Systems
1 Introduction
2 Preliminaries
3 Linear Hybrid Systems
3.1 Semantics
3.2 Special Subclasses of Linear Hybrid Automata
3.3 Parallel Composition of Linear Hybrid Automata
4 Timed Language Equivalence of PMHS and Timed Automata
5 Main Result
6 A Decidable Class of Multi-rate Automata
7 Conclusion
References
Contracts for Schedulability Analysis
1 Introduction and Related Work
2 Scheduling Components
2.1 Our Approach: Building on Top of Assume/Guarantee Contracts
2.2 Concrete Scheduling Components
2.3 Abstract Scheduling Components
2.4 Faithfulness of the Mapping
3 Scheduling Contracts
3.1 Getting Sub-contracts in the AUTOSAR Development Process
4 An Example in the Context of AUTOSAR
5 Conclusion
References
Bounded Determinization of Timed Automata with Silent Transitions
1 Introduction
2 Timed Automata with Silent Transitions
3 k-Bounded Unfolding of Timed Automata
3.1 Renaming the Clocks
4 Removing the Silent Transitions
5 Determinization
6 Complexity
7 Implementation and Experimental Results
8 Related Work
9 Conclusion
References
A Score Function for Optimizing the Cycle-Life of Battery-Powered Embedded Systems
1 Introduction
2 Uppaal Stratego
3 Battery Concepts
4 The Wear Score Function for SOC-Profiles
5 Nano-satellite Case Study
5.1 System Description
5.2 Satellite Model
5.3 Learning and Optimization
6 Discussion of the Wear Score Function
6.1 Limitations
7 Related Work
8 Conclusion
References
A Appendix
Author Index

System requirements

Save as PDF Copy link into clipboard

Schweitzer Fachinformationen

Formal Modeling and Analysis of Timed Systems

Description

More details

Other editions

Additional editions

Content

System requirements