Software Engineering and Formal Methods

Name: Software Engineering and Formal Methods | 17th International Conference, SEFM 2019, Oslo, Norway, September 18-20, 2019, Proceedings
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

17th International Conference, SEFM 2019, Oslo, Norway, September 18-20, 2019, Proceedings

Peter Csaba Ölveczky Gwen Salaün(Herausgeber*in)

Springer (Verlag)

Erschienen am 9. September 2019

XVIII, 550 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-030-30446-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
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 Case
1 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 Systems
Automatic 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 Logic
3 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 Module
4.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
3.3 Compilation of Our DSL to a Feature Model
3.4 Resolving Differing Credit Points
4 Evaluation
4.1 Tool Support for Implementation
4.2 At-Most-k Encoding Performance Comparison
4.3 Branches Evaluation
4.4 Threats to Validity
5 Related Work
6 Conclusion and Future Work
References
Software Evolution with a Typeful Version Control System
1 Introduction
2 The Journey of a Class
3 Versioned Featherweight Java
4 Future Work
5 Related Work
6 Conclusions
References
Compositional Feature-Oriented Systems
1 Introduction
2 Theoretical Foundations
2.1 Feature Models
2.2 Featured Transition Systems
2.3 Featured Programs
3 Compositional Feature-Oriented Systems
4 Family-Ready Systems
4.1 Parallel Composition
4.2 Superimposition
4.3 Dynamics and Family Models
5 Between Composition Worlds
5.1 From Parallel Composition to Superimposition
5.2 From Superimposition to Parallel Composition
6 Concluding Remarks
References
Model-Based Testing
Multi-objective Search for Effective Testing of Cyber-Physical Systems
1 Introduction
2 Related Work
3 Preliminaires
3.1 Analysis of Cyber-Physical Systems
4 Finding Inputs via Search-Based Heuristics
4.1 Search Based Inputs and Critical Epsilon
4.2 Notions of Coverage
4.3 A Notion of Diversity
4.4 Mechanisation
5 Empirical Analysis
5.1 Case Study
5.2 Experimental Plan
5.3 Results
6 Conclusions and Future Work
References
Mutation Testing with Hyperproperties
1 Introduction
2 Preliminaries
2.1 System Model
2.2 HyperLTL
3 Killing Mutants
3.1 Mutants
3.2 Killing
4 Killing with Hyperproperties
4.1 Deterministic Case
4.2 Non-deterministic Case
5 Non-deterministic Models in Practice
5.1 Controlling Non-determinism in STS
5.2 Controlling Non-determinism in Modeling Languages
6 Experiments
6.1 Toolchain
7 Related Work
8 Conclusion
References
Test Model Coverage Analysis Under Uncertainty
1 Introduction
2 Preliminary: Probabilistic Models and Simple Coverage
2.1 Representing a Test Case: Execution Model
3 Coverage Under Uncertainty
4 Efficient Coverage Calculation
4.1 Non-simple Sentences
4.2 Coverage of Aggregate Goals
5 Experimental Results
6 Related Work
7 Conclusion
References
Model Inference
Learning Minimal DFA: Taking Inspiration from RPNI to Improve SAT Approach
1 Introduction
2 Definitions
3 Inference Problem
3.1 RPNI Method
3.2 SAT Solving Approach
4 Incremental SAT Solving with Domain Specific Heuristics
4.1 Incremental SAT Solving
4.2 Domain Specific Heuristics
5 Experimental Evaluation
5.1 Inference Varying the Number of Examples
5.2 Inference from Learning Samples of Growing Generators
6 Conclusion
References
Incorporating Data into EFSM Inference
1 Introduction
2 Background
3 Extending the Inference Process
3.1 PTA Construction
3.2 Merging States
3.3 Resolving Nondeterminism by Merging Transitions
4 Introducing Registers
4.1 The Store and Reuse Heuristic
4.2 The Increment and Reset Heuristic
4.3 The Same Register Use Heuristic
5 Implementation
5.1 Checking Context Properties
6 Evaluation
7 Conclusions and Future Works
References
Ontologies and Machine Learning
Isabelle/DOF: Design and Implementation
1 Introduction
2 Background: The Document Model
3 The DOF Design
3.1 Ontology Modeling in ODL
3.2 Meta-Types as Types
3.3 Annotating with Ontology Meta-Data: Outer Syntax
3.4 Editing Documents with Ontology Meta-Data: Inner Syntax
3.5 ODL Class Invariants
3.6 ODL Monitors
3.7 Document Representation
4 The Isabelle/DOF Implementation
4.1 Writing Isabelle/DOF as User-Defined Plugin in Isabelle/Isar
4.2 Programming Antiquotations
4.3 Implementing Second-Level Type-Checking
4.4 Programming Class Invariants
4.5 Implementing Monitors
4.6 Document Representation
5 Conclusion and Related Work
5.1 Related Work
5.2 Conclusion
References
Towards Logical Specification of Statistical Machine Learning
1 Introduction
2 Preliminaries
2.1 Notations
2.2 Syntax of StatEL
2.3 Distributional Kripke Model
2.4 Stochastic Semantics of StatEL
3 Techniques for Conditional Indistinguishability
3.1 Counterfactual Epistemic Operators
3.2 Conditional Indistinguishability via Counterfactual Knowledge
4 Formal Model for Statistical Classification
4.1 Statistical Classification Problems
4.2 Modeling the Behaviours of Classifiers
4.3 Modeling the Non-deterministic Inputs from Adversaries
5 Formalizing the Classification Performance
6 Formalizing the Robustness of Classifiers
6.1 Total Correctness of Classifiers
6.2 Probabilistic Robustness Against Targeted Attacks
6.3 Probabilistic Robustness Against Non-targeted Attacks
7 Formalizing the Fairness of Classifiers
7.1 Group Fairness (Statistical Parity)
7.2 Individual Fairness (as Lipschitz Property)
7.3 Equal Opportunity
8 Related Work
9 Conclusion
A Proof for Proposition 1
References
Operating Systems
Efficient Formal Verification for the Linux Kernel
1 Introduction
2 Background
2.1 Automata and Discrete Event System
2.2 Linux Tracing
3 Related Work
3.1 Automata-Based Linux Modelling
3.2 Formal Methods and OS Kernels
3.3 Formal Methods and the Linux Kernel Community
4 Efficient Formal Verification for the Linux Kernel
5 Performance Evaluation
5.1 Throughput Evaluation
5.2 Latency Evaluation
6 Conclusions and Future Work
References
Reproducible Execution of POSIX Programs with DiOS
1 Introduction
1.1 Contribution
1.2 Design Goals
1.3 Related Work
2 Platform Interface
2.1 Preliminaries
2.2 Program Memory
2.3 Execution Stack
2.4 Auxiliary Interfaces
3 Supported Platforms
3.1 DiVM
3.2 KLEE
3.3 Native Execution
4 Design and Architecture
4.1 Kernel Components
4.2 Thread Support
4.3 System Calls
4.4 The C Library
4.5 C++ Support Libraries
4.6 Binary Compatibility
5 Evaluation
5.1 Verification with DiVM
5.2 Portability
5.3 API and ABI Coverage and Compatibility
6 Conclusions and Future Work
References
Program Analysis
Using Relational Verification for Program Slicing
1 Introduction
2 Static Backward Slicing
3 Relational Verification of Slice Candidates
4 A Framework for Automatic Slicing
4.1 Removing Instructions Based on Heuristics
4.2 Counterexample Guided Slicing
5 Discussion
6 Related Work
7 Conclusion and Future Work
References
Local Nontermination Detection for Parallel C++ Programs
1 Introduction
2 Related Work
3 Preliminaries
3.1 State Space of a Program
3.2 Resource Sections
4 Local Nontermination
5 Detection of Nontermination
5.1 Detection Algorithm
5.2 Scheduling and Fairness
5.3 Implementation and Usage
5.4 Interaction with Other Features of DIVINE
6 Evaluation
7 Conclusion
References
Relating Models and Implementations
An Implementation Relation for Cyclic Systems with Refusals and Discrete Time
1 Introduction
2 Testing Context and Related Work
3 Background and Models
3.1 Traces and Automata
3.2 Timed Models
3.3 A First Implementation Relation
4 An Implementation Relation Including Refusals
5 Alternative Characterisations
5.1 Using an Automaton
5.2 Using Observers
6 Conclusions and Future Work
References
Modular Indirect Push-Button Formal Verification of Multi-threaded Code Generators
1 Introduction
2 Preliminaries
3 Slco and the Generation of Java Code
4 Verification of Code Generation
4.1 Verification Overview
4.2 Constructing and Comparing CFGs
4.3 Verification of Transition Methods
4.4 Supporting the Complete Slco Language
5 Implementation and Experiments
6 Related Work
7 Conclusions
References
Runtime Verification
An Operational Guide to Monitorability
1 Introduction
2 Preliminaries
3 A Monitor-Oriented Hierarchy
4 An Instantiation for Regular Properties
5 A Syntactic Characterisation of Monitorability
6 Safety and Co-safety
7 Pnueli and Zaks
8 Monitorability in Other Settings
9 Conclusion
References
Let's Prove It Later-Verification at Different Points in Time
1 Introduction
2 Self-verification
3 Case Study
3.1 Informal Description
3.2 Formal Specification
3.3 When to Verify
4 Realization
4.1 A Design Flow for Self-verification
4.2 The Demonstrator
5 Discussion and Conclusions
5.1 When to Prove
5.2 Conclusions
References
Security
Using Threat Analysis Techniques to Guide Formal Verification: A Case Study of Cooperative Awareness Messages
1 Introduction
1.1 Methodology
2 Background and Related Work
3 Threat Analysis of CAM
3.1 Specialising STRIDE for CAM
3.2 Considering the Threats
4 Model-Checking with Promela/SPIN
4.1 Basic Scenario: Safety
4.2 Investigating Spoofing
4.3 Discussion
5 Deductive Verification with Dafny
5.1 Sending CAMs
5.2 Receiving CAMs
5.3 Discussion
6 Conclusions and Future Work
References
Towards Detecting Trigger-Based Behavior in Binaries: Uncovering the Correct Environment
1 Introduction
2 Background
3 Methodology
3.1 Symbolic Summary Functions
3.2 Approach to Symbolic Execution
4 Implementation
4.1 Symbolic Summaries for System Calls
4.2 Control Flow Graph
4.3 Call Stack Management
4.4 Model of the Execution State
5 Evaluation
5.1 Setting Up Our Experiment
5.2 Results
6 Conclusion
References
Verification
Formal Verification of Rewriting Rules for Dynamic Fault Trees
1 Introduction
2 DFT Rewrite Rules
2.1 Rewrite Framework
2.2 Rewrite Rules
2.3 Non-structural Rules
3 DFT Theory in HOL4
4 HOL Formalization of n-ary DFT Gates
5 Formal Verification of Rewriting Rules
6 Conclusions
References
Partially Bounded Context-Aware Verification
1 Introduction
2 Background and Related Work
3 A Language for Context Guided Reachability: xGDL
3.1 xGDL Abstract Syntax
3.2 xGDL Operational Semantics
3.3 xGDL Compilation
3.4 xGDL Guide and Closed System Composition
3.5 Partially Bounded Verification
4 Case-Study: The Landing Gear System
4.1 LGS Executable Model
4.2 xGDL Verification Guides
5 Conclusion and Perspectives
References
Author Index

Systemvoraussetzungen

Als PDF speichern Als Link merken