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(Herausgeber*in)

Springer (Verlag)

Erschienen am 21. August 2015

X, 321 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-319-22975-1 (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

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

Systemvoraussetzungen

Als PDF speichern Als Link merken