Formal Modeling and Analysis of Timed Systems [[electronic resource] ] : 13th International Conference, FORMATS 2015, Madrid, Spain, September 2-4, 2015, Proceedings / / edited by Sriram Sankaranarayanan, Enrico Vicario

• Pubblicazione: Cham : , : Springer International Publishing : , : Imprint : Springer, , 2015
• Edizione: 1st ed. 2015.
• Descrizione fisica: 1 online resource (X, 321 p. 90 illus.)
• Disciplina: 003.3
• Soggetto topico: Computer science; Software engineering; Application software; Machine theory; Theory of Computation; Computer Science Logic and Foundations of Programming; Software Engineering; Computer and Information Systems Applications; Formal Languages and Automata Theory
• Persona (resp. second.): SankaranarayananSriram; VicarioEnrico
• Note generali: Bibliographic Level Mode of Issuance: Monograph
• Nota di contenuto: 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.
• Sommario/riassunto: This book constitutes the refereed proceedings of the 13th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2015, held in Madrid, Spain, in September 2015. The conference was organized under the umbrella of Madrid Meet 2015, a one week event focussing on the areas of formal and quantitative analysis of systems, performance engineering, computer safety, and industrial critical applications. The 19 papers presented in this volume were carefully reviewed and selected from 42 initial submissions.
• Titolo autorizzato: Formal Modeling and Analysis of Timed Systems
• ISBN: 3-319-22975-3
• Formato: Materiale a stampa
• Livello bibliografico: Monografia
• Lingua di pubblicazione: Inglese
• Record Nr.: 9910483460503321
• Lo trovi qui: Univ. Federico II
• Serie: Theoretical Computer Science and General Issues, . 2512-2029 ; ; 9268