Linked e-resources
Details
Table of Contents
Intro; Preface; Organization; Abstracts of Invited Talks; Security Protocols: Model Checking Standards; Automated Test Generation: A Journey from Symbolic Execution to Smart Fuzzing and Beyond; Contents; Invited Paper; Object-Centric Process Mining: Dealing with Divergence and Convergence in Event Data; 1 Introduction; 2 Related Work on Object-Centric Process Mining; 3 The Problem; 4 Defining Event Data; 5 A Baseline Discovery Approach; 6 Beyond Directly-Follows Graphs; 7 Conclusion; References; Cooperative Asynchronous Systems
Relating Session Types and Behavioural Contracts: The Asynchronous Case1 Introduction; 2 Behavioural Contracts; 3 Asynchronous Session Types; 4 Mapping Session Types into Behavioural Contracts; 5 Related Work and Conclusion; References; Asynchronous Cooperative Contracts for Cooperative Scheduling; 1 Introduction; 2 Method Contracts for Asynchronous Method Calls; 2.1 Specifying State in an Asynchronous Setting; 2.2 Specifying Interleavings; 2.3 Composition; 3 An Active Object Language; 4 Formalizing Method Contracts; 5 Verification; 6 Related Work and Conclusion; References
Cyber-Physical SystemsAutomatic Failure Explanation in CPS Models; 1 Introduction; 2 Background; 2.1 Signals and Signal Temporal Logic; 2.2 Daikon; 3 Case Study; 4 Failure Explanation; 4.1 Testing; 4.2 Mining; 4.3 Explaining; 5 Empirical Evaluation; 5.1 Scope Reduction, Cause Detection and Qualitative Analysis; 5.2 Computation Time; 5.3 Evaluation by Professional Engineers; 6 Related Work; 7 Future Work and Conclusions; References; Evolution of Formal Model-Based Assurance Cases for Autonomous Robots; 1 Introduction; 2 Background and Formal Preliminaries; 2.1 Assurance Cases
2.2 Isabelle/UTP and Differential Dynamic Logic3 Formal Model-Based Assurance Cases; 3.1 Assurance Case Construction; 3.2 Assurance Case Extension; 4 Application to Mobile Ground Robot; 4.1 [0]: Initial Assurance Case; 4.2 [1]: First Extension; 4.3 [2]: Second Extension; 5 Discussion; 6 Conclusions; References; Towards Integrating Formal Verification of Autonomous Robots with Battery Prognostics and Health Management; 1 Introduction; 2 Background; 2.1 Probabilistic Model Checking; 2.2 Battery Modelling and PHM; 3 The Running Example; 4 The Modelling in PRISM; 4.1 The Drone Module
4.2 The Grid Module4.3 The Environment Module; 4.4 The Battery Module; 5 Results; 5.1 Effects of Battery Safety Strategies and Dynamic Environments; 5.2 Comparison of Models, Disregarding the Battery Features; 6 Related Work; 7 Discussions, Conclusions and Future Work; References; Feature-Oriented and Versioned Systems; SAT Encodings of the At-Most-k Constraint; 1 Introduction; 2 Encoding At-Most-k Constraints; 3 Modelling Configuration of University Courses as Feature Models; 3.1 Formalizing Branches of Study; 3.2 A DSL to Describe Fields and Branches of Study
Relating Session Types and Behavioural Contracts: The Asynchronous Case1 Introduction; 2 Behavioural Contracts; 3 Asynchronous Session Types; 4 Mapping Session Types into Behavioural Contracts; 5 Related Work and Conclusion; References; Asynchronous Cooperative Contracts for Cooperative Scheduling; 1 Introduction; 2 Method Contracts for Asynchronous Method Calls; 2.1 Specifying State in an Asynchronous Setting; 2.2 Specifying Interleavings; 2.3 Composition; 3 An Active Object Language; 4 Formalizing Method Contracts; 5 Verification; 6 Related Work and Conclusion; References
Cyber-Physical SystemsAutomatic Failure Explanation in CPS Models; 1 Introduction; 2 Background; 2.1 Signals and Signal Temporal Logic; 2.2 Daikon; 3 Case Study; 4 Failure Explanation; 4.1 Testing; 4.2 Mining; 4.3 Explaining; 5 Empirical Evaluation; 5.1 Scope Reduction, Cause Detection and Qualitative Analysis; 5.2 Computation Time; 5.3 Evaluation by Professional Engineers; 6 Related Work; 7 Future Work and Conclusions; References; Evolution of Formal Model-Based Assurance Cases for Autonomous Robots; 1 Introduction; 2 Background and Formal Preliminaries; 2.1 Assurance Cases
2.2 Isabelle/UTP and Differential Dynamic Logic3 Formal Model-Based Assurance Cases; 3.1 Assurance Case Construction; 3.2 Assurance Case Extension; 4 Application to Mobile Ground Robot; 4.1 [0]: Initial Assurance Case; 4.2 [1]: First Extension; 4.3 [2]: Second Extension; 5 Discussion; 6 Conclusions; References; Towards Integrating Formal Verification of Autonomous Robots with Battery Prognostics and Health Management; 1 Introduction; 2 Background; 2.1 Probabilistic Model Checking; 2.2 Battery Modelling and PHM; 3 The Running Example; 4 The Modelling in PRISM; 4.1 The Drone Module
4.2 The Grid Module4.3 The Environment Module; 4.4 The Battery Module; 5 Results; 5.1 Effects of Battery Safety Strategies and Dynamic Environments; 5.2 Comparison of Models, Disregarding the Battery Features; 6 Related Work; 7 Discussions, Conclusions and Future Work; References; Feature-Oriented and Versioned Systems; SAT Encodings of the At-Most-k Constraint; 1 Introduction; 2 Encoding At-Most-k Constraints; 3 Modelling Configuration of University Courses as Feature Models; 3.1 Formalizing Branches of Study; 3.2 A DSL to Describe Fields and Branches of Study