Integrated Formal Methods

Name: Integrated Formal Methods | 15th International Conference, IFM 2019, Bergen, Norway, December 2-6, 2019, Proceedings
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

15th International Conference, IFM 2019, Bergen, Norway, December 2-6, 2019, Proceedings

Wolfgang Ahrendt Silvia Lizeth Tapia Tarifa(Herausgeber*in)

Springer (Verlag)

Erschienen am 22. November 2019

XVII, 554 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-030-34968-4 (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
Deductive Verification of OCaml Libraries
Safe Deep Neural Networks
Contents
Invited Talk
The Digital Thread in Industry 4.0
1 From the Digital Twin to the Digital Thread
2 Bringing the UR3 Controller in the Web
2.1 Programming the UR3
2.2 Case Study: A Web UR3 Controller
3 DIME as a Model Driven IDE for Robotics
3.1 Behavioural Models and Feature DSL
3.2 The UR3 Native DSL
3.3 GUI Models and Their DSL
4 XMDD for the Digital Thread
4.1 Innovation Directions
4.2 Experiential Evidence so Far
References
Regular Papers
Accelerating Parameter Synthesis Using Semi-algebraic Constraints
1 Introduction
2 CTL Parameter Synthesis
2.1 Parameter Synthesis Problem
2.2 Parallel Lock-Free Algorithm
3 Semi-algebraic Sets as Cylindrical Decompositions
3.1 Preliminaries
3.2 Method Overview
3.3 Open CAD Construction
3.4 Reduced CAD Tree
4 Evaluation
5 Conclusions
References
Uniqueness Types for Efficient and Verifiable Aliasing-Free Embedded Systems Programming
1 Introduction
2 Overview
2.1 Aliasing-Free Programming
2.2 Uniqueness Types for High-Performance Aliasing-Free Programming
3 Type and Permission System
3.1 Uniqueness Annotation
3.2 Uniqueness Semantics
3.3 Permissions
3.4 Rules
4 Formalization
4.1 Syntax
4.2 Operational Semantics
4.3 Type and Permission System
4.4 Soundness
5 Implementation
6 Validation
6.1 Annotation Overhead
6.2 Performance Benchmark
7 Related Work
8 Conclusion
References
Using Ontologies in Formal Developments Targeting Certification
1 Introduction
2 Background
2.1 Isabelle and HOL
2.2 The Isabelle/DOF Framework
2.3 A Guided Tour Through ODL
3 The Underlying Methodology
4 A Case-Study: An Odometer-Subsystem
4.1 System Requirements Specification as an Integrated Source
4.2 Formal Enrichment of the Software Requirements Specification
4.3 Verification of the Software Requirements Specification
5 The CENELEC Ontology
5.1 Tracking Concepts and Definitions
5.2 Major Ontological Entities: Requirements and Evidence
5.3 Tracking Claims, Derived Requirements and Evidence
6 Ontological Embedding and Compliance
7 Generating Document Variants
8 Related Work
9 Conclusion
References
A Program Logic for Dependence Analysis
1 Introduction
2 Program Logic and Calculus
2.1 Syntax
2.2 Semantics
2.3 Calculus
2.4 Memory Locations and Heap in JavaDL
3 Dependence-Aware Program Logic
3.1 Formal Semantics of Read and Write Dependences
3.2 Memory Access Updates
3.3 Specification of Data Dependence Properties
3.4 Verification of Data Dependence Properties
4 Experiments
5 Related Work
6 Future Work and Conclusion
References
Evaluation of Program Slicing in Software Verification
1 Introduction
1.1 Related Work
2 Program Slicing
2.1 Slicing Programs Using Dependence Graphs
2.2 Program Slicing in Verification
3 Considered Tools
3.1 Symbiotic
3.2 Slicing Algorithm
3.3 Verification Tools and Their Integration
4 Experiments and Evaluation
5 Conclusion
References
Integrated Model-Checking for the Design of Safe and Efficient Distributed Software Commissioning
1 Introduction
2 Madeus and Petri Nets
3 MADA
3.1 From Madeus to Petri Nets
3.2 Property Language and Temporal Logic
4 Evaluation
4.1 MADA Evaluation
4.2 Discussion
5 Related Work
6 Conclusion
References
Learning to Reuse: Adaptive Model Learning for Evolving Systems
1 Introduction
2 Background
2.1 Finite State Machines
2.2 Model Learning
2.3 Adaptive Learning
3 The partial-Dynamic L*M Algorithm
3.1 (Step 1) On-the-Fly Exploration of the Reused Table
3.2 (Step 2) Building an Experiment Cover Tree
3.3 (Step 3) Running L*M Using the Outcomes of L*M
4 Empirical Evaluation
4.1 Research Questions
4.2 Subject Systems
4.3 Experiment Design
4.4 Analysis of Results
4.5 Threats to Validity
5 Conclusions and Future Work
References
Axiomatic Characterization of Trace Reachability for Concurrent Objects
1 Introduction
2 The Programming Language
3 Axiomatization
4 Program Synthesis
5 Future Extensions
6 Discussion
References
Dynamic Reconfigurations in Frequency Constrained Data Flow
1 Introduction
2 Motivation
3 The Polygraph Modeling Language
3.1 Background
3.2 Additional Properties of Polygraph Executions
3.3 Mode Extension of the Polygraph Modeling Language
4 Method and Tool Support to Check Coherence
5 Discussion and Related Work
6 Conclusion
References
Ontology-Mediated Probabilistic Model Checking
1 Introduction
2 Preliminaries
2.1 Markov Decision Processes
2.2 Stochastic Programs
2.3 Description Logics
3 Ontologized Programs
3.1 Ontologizing Stochastic Programs
3.2 Semantics of Ontologized Programs
4 Analysis of Ontologized Programs
5 Evaluation
6 Related Work
7 Discussion and Future Work
References
Fuzzing JavaScript Environment APIs with Interdependent Function Calls
1 Introduction
2 Prototype Graphs
3 Interdependent Function Calls
4 Experimental Results
5 Related Work
6 Summary
References
Dione: A Protocol Verification System Built with Dafny for I/O Automata
1 Introduction
2 Background: Brief Overview of IOA
3 Overview of Dione
3.1 Dione Language
3.2 Translating Dione to Dafny
3.3 Bounded Model Checking and k-Induction with Dafny
4 Case Studies with Dione
4.1 Self-stabilization Protocol on a Bidirectional Array
4.2 Self-stabilization Protocol on a Ring
4.3 Asynchronous Leader Election on a Ring
4.4 CAN bus Arbitration
5 Conclusion
References
Relating Alternating Relations for Conformance and Refinement
1 Introduction
2 Preliminaries
3 Two Preorders on Interface Automata
3.1 Input-Failure Refinement
3.2 Input Universal/Output Existential Traces
4 Characterizing uioco
5 Game Characterizations
5.1 Alternating-Trace Containment for IA
5.2 The Game of Input-Failure Refinement
6 Alternating Simulation
7 Conclusion and Future Work
References
Embedding SMT-LIB into B for Interactive Proof and Constraint Solving
1 Introduction and Motivation
2 Introductory Examples
3 Translating SMT-LIB to B
3.1 If-Then-Else
3.2 Let
3.3 Formal Definition of Translation
4 Interactive Proof Using Atelier B
5 Constraint Solving Using ProB
6 Related Work
7 Future Work
8 Discussion and Conclusion
References
An Integrated Approach to a Combinatorial Optimisation Problem
1 Introduction
2 Problem Motivation and Informal Description
3 Related Work and Justification of an SMT Approach
4 Formal Model of the Problem and of Its Solution
4.1 Paths Calculation
4.2 Interaction Constraints
5 SMT Translation
6 Verification
6.1 First Step: Generating SMT-LIB Code from Theorem Hypotheses
6.2 Second Step: Linking Generated SMT Code to the Existing Code
7 Conclusions
References
Computing Bisimilarity Metrics for Probabilistic Timed Automata
1 Introduction
2 Background
2.1 Probabilistic LTS and Bisimulation Metrics
2.2 Probabilistic Timed Automata
3 Zone Graph
3.1 Zone Graphs in Normal Form
3.2 Action and Timed Transitions over Zones
4 Computing n-Bisimilarity Metric
4.1 Action Transitions
4.2 Timed Transitions
4.3 Computing Kantorovich Lifting
4.4 Computing Bisimilarity Metrics
5 Future Work
References
Sound Probabilistic Numerical Error Analysis
1 Introduction
2 Background
3 Tracking Probabilistic Errors
3.1 Probabilistic Interval Subdivision
3.2 Probabilistic Roundoff Error Analysis
3.3 Probabilistic Analysis with Approximate Error Specification
3.4 Implementation
4 Experimental Evaluation
5 Related Work
6 Conclusion
References
Automated Drawing of Railway Schematics Using Numerical Optimization in SAT
1 Introduction
2 Problem Definition and Formalization
2.1 Linear Positioning System
2.2 Track Network Representation
2.3 Linear Schematic Drawing
3 Model Definitions and Drawing Algorithms
3.1 Vertical Ordering Relation on Edges
3.2 Level-Based Linear Programming Encoding
3.3 Level-Based SAT Encoding
3.4 Cross-Section SAT Encoding
3.5 Symbols and Labels
4 Tool Usage
5 Conclusions and Future Work
References
Asynchronous Testing of Synchronous Components in GALS Systems
1 Introduction
2 GRL Model of an Autonomous Car
3 Model Checking and Conformance Test Generation
3.1 Model Checking
3.2 Conformance Test Generation
4 Testing Techniques for Synchronous Components
5 Test Projection and Exploration
5.1 Test Graph Projection
5.2 Translating and Renaming
5.3 Test Graph Exploration
6 Related Work
7 Conclusion
References
Isabelle/SACM: Computer-Assisted Assurance Cases with Integrated Formal Methods
1 Introduction
2 Preliminaries
3 Case Study: Tokeneer
4 Isabelle/SACM
4.1 Modelling: Embedding SACM in Isabelle
4.2 Interactive Assurance Language (IAL)
5 Modelling and Verification of Tokeneer
5.1 Modelling and Mechanisation
5.2 Formal Verification of SFR1
6 Mechanising the Tokeener Assurance Case
7 Related Work
8 Conclusions
References
Practical Abstractions for Automated Verification of Message Passing Concurrency
1 Introduction
2 Programs and Processes
2.1 Programs
2.2 Processes
3 Verification Example
4 Formalisation
4.1 Program Logic
4.2 Program Judgments
4.3 Soundness
5 Extensions
6 Related Work
7 Conclusion
References
Formal Verification of an Industrial Safety-Critical Traffic Tunnel Control System
1 Introduction
1.1 Contributions and Outline
2 Preliminaries
2.1 Modelling and Analysis with mCRL2
2.2 Deductive Verification with VerCors
3 Informal Tunnel Software Specification
3.1 Structure of the FSM
3.2 Pseudo Code Specification
4 Modelling the Tunnel Control System Using mCRL2
5 Analysing the Tunnel Control System with mCRL2
6 Specification Refinement Using VerCors
7 Related Work
8 Conclusion
References
Resource Sharing via Capability-Based Multiparty Session Types
1 Introduction
2 Multiparty Session -Calculus with Capabilities
3 Multiparty Session Types with Capabilities
4 Case Study: Producer-Consumer
5 Technical Results
6 Related Work, Conclusion and Future Work
References
A Multi-target Code Generator for High-Level B
1 Introduction and Motivation
2 Steps of Code Generation
3 Code Generation in Practice
3.1 Template-Based Code Generation
3.2 Code Generation with StringTemplate and B AST
3.3 Extensibility for Other Programming Languages
3.4 Implementation of B Data Types
3.5 Quantified and Non-deterministic Constructs
3.6 Identifier Clash Problem with Keywords
4 Performance Considerations and Evaluation
5 Related Work
6 Discussion, Conclusion and Future Work
References
Visualization and Abstractions for Execution Paths in Model-Based Software Testing
1 Introduction
2 Extended Finite State Machines and Modbat
3 Execution Paths and Representation
4 Path Coverage Visualization
5 State-Based and Path-Based Graphs
5.1 State-Based Graphs
5.2 Path-Based Graphs
5.3 User-Defined Search Function
6 Experimental Evaluation
7 Related Work
8 Conclusions and Future Work
References
Short Papers
HYPpOTesT: Hypothesis Testing Toolkit for Uncertain Service-Based Web Applications
1 Introduction
2 Running Example: The U-Store Web Application
3 The Hypothesis Testing Toolkit
4 Evaluation
5 Conclusion
References
Interactive Visualization of Saturation Attempts in Vampire
1 Introduction
2 Proof Search in Vampire
3 Analysis of Saturation Attempts of Vampire
4 Implementation of SatVis 1.0
5 Conclusion
References
SIGmA: GPU Accelerated Simplification of SAT Formulas
1 Introduction
2 SIGmA Functionality and Architecture
3 Benchmarks
4 Conclusion
References
Journal-First Extended Abstracts
Summary of: Dynamic Structural Operational Semantics
1 Short Introduction to Dynamic SOS
2 An Illustrative Example
3 Dynamic SOS
References
Summary of: An Evaluation of Interaction Paradigms for Active Objects
1 Introduction
2 Future Mechanisms
3 A High-Level, Future-Less Language for Active Objects
4 Comparison
5 Conclusion
References
Summary of: On Checking Delta-Oriented Software Product Lines of Statecharts
1 Background
2 Contributions of LIENHARDTspsetspsalspsSCPsps2018
3 Conclusion and Future Work
References
A Summary of Formal Specification and Verification of Autonomous Robotic Systems
1 Introduction and Methodology
2 Answering the Research Questions
3 Conclusion
References
Summary of: On the Expressiveness of Modal Transition Systems with Variability Constraints
1 Background
2 Contributions
3 Conclusion and Future Work
References
Summary of: A Framework for Quantitative Modeling and Analysis of Highly (re)configurable Systems
References
Author Index

Systemvoraussetzungen

Als PDF speichern Als Link merken