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(Editor)

Springer (Publisher)

Published on 9. September 2019

XVIII, 550 pages

E-Book

PDF with digital watermarking

System requirements

978-3-030-30446-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
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

System requirements

Save as PDF Copy link into clipboard

Schweitzer Fachinformationen

Software Engineering and Formal Methods

Description

More details

Other editions

Additional editions

Content

System requirements