Formal Methods

Name: Formal Methods | 22nd International Symposium, FM 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 15-17, 2018, Proceedings
Brand: Springer
Price: 96.29 EUR
Availability: OnlineOnly

22nd International Symposium, FM 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 15-17, 2018, Proceedings

Klaus Havelund Jan Peleska Bill Roscoe Erik de Vink(Herausgeber*in)

Springer (Verlag)

Erschienen am 11. Juli 2018

XIV, 692 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-319-95582-7 (ISBN)

96,29 €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
Contents
Invited Papers
Processing Text for Privacy: An Information Flow Perspective
1 Introduction
2 Text Document Processing
2.1 Representing Documents for Topic Classification and Author Identification
2.2 Privacy Versus Utility
3 Channels, Secrets and Information Flow
3.1 Vulnerability Induced by Gain-Functions
3.2 Privacy Mechanisms as Channels
3.3 Attacks on Simple Confusability
3.4 Universal Confusability
3.5 Differential Privacy
3.6 Privacy Versus Utility
4 Generalised Differential Privacy and Obfuscation
4.1 Experiments
5 Conclusions and Future Work
References
20Years of Real Real Time Model Validation
1 Introduction
2 The Uppaal Tool Suite
3 Verification
4 Testing
5 Planning, Scheduling and Synthesis
6 Lessons Learned
References
FM 2018 Main Conference
Deadlock Detection for Actor-Based Coroutines
1 Introduction
2 The Programming Language
3 The Concrete System
4 The Abstract System
5 Correctness of Predicate Abstraction
6 Decidability of Deadlock Detection
7 Conclusion
References
An Algebraic Approach for Reasoning About Information Flow
1 Introduction
2 Preliminaries
3 Operators on Channel Composition
3.1 The Parallel Composition Operator
3.2 The Visible Choice Operator p
3.3 The Hidden Choice Operator p
3.4 A Compositional Description of the Dining Cryptographers
4 Algebraic Properties of Channel Operators
4.1 Properties Regarding Channel Operators
4.2 Properties Regarding Cascading
5 Information Leakage of Channel Operators
5.1 The Problem of Compositional Vulnerability
5.2 The Problem of Relative Monotonicity
6 Case Study: The Crowds Protocol
7 Related Work
8 Conclusions and Future Work
References
Towards `Verifying' a Water Treatment System
1 Introduction
2 Background
3 Our Approach
3.1 The Model
3.2 Learning Algorithm
3.3 Verification
3.4 Abstraction Refinement
3.5 Overall Algorithm
4 Case Study Results
5 Conclusion and Related Work
References
FSM Inference from Long Traces
1 Introduction
2 Definitions
3 Passive Inference
3.1 Problem Statement
3.2 Encoding as a SAT Problem
3.3 Auxiliary Variables
3.4 Symmetry Breaking
4 Incremental Inference
4.1 Prefix-Based Method
4.2 Suffix-Based Method
4.3 Discussion
5 Industrial Case Study
6 Conclusion
References
A Weakness Measure for GR(1) Formulae
1 Introduction
2 Related Work
3 Preliminaries
4 Problem Statement
5 Weakness Measure of GR(1) Formulae
5.1 Dimension of Invariants
5.2 Fairness and Fairness Complements
5.3 Dimension Pairs for GR(1) Formulae
5.4 Initial Conditions
6 Evaluation
7 Conclusion
References
Producing Explanations for Rich Logics
1 Introduction
2 The Propositional µ-Calculus
3 A µ-Calculus-Based Framework for Rich Explanations
3.1 Translation of ATL Models and Formulas to µ-calculus
3.2 µ-Calculus Explanations
3.3 Translating µ-Calculus Explanations
4 Implementation
5 Application to ATL
6 Related Work
7 Conclusion
References
The Compound Interest in Relaxing Punctuality
1 Introduction
2 Preliminaries
3 Metric Interval Regular Expressions
4 From MIRE to Deterministic Timed Automata
5 Metric Interval Dynamic Logic
6 From MIDL to Nondeterministic Timed Automata
7 Discussion
References
IPL: An Integration Property Language for Multi-model Cyber-physical Systems
1 Introduction
2 Motivating Integration Case
3 Related Work
4 Integration Property Language: Design
5 Integration Property Language: Details
5.1 Concepts and Preliminaries
5.2 Syntax
5.3 Semantics
5.4 Verification Algorithm
6 Evaluation
6.1 Case Study: Adaptive Mobile Robot
7 Discussion
References
Timed Epistemic Knowledge Bases for Social Networks
1 Introduction
2 A Timed Knowledge Based Logic
2.1 Syntax
2.2 Semantics
2.3 Model Checking KBLRT
2.4 Properties of the Framework
3 Writing Privacy Policies
4 Related Work and Concluding Remarks
References
Optimal and Robust Controller Synthesis
1 Introduction
2 Energy Timed Automata
3 Energy Timed Automata with Uncertainties
4 Case Study
5 Conclusion
References
Encoding Fairness in a Synchronous Concurrent Program Algebra
1 Introduction
2 Synchronous Concurrent Refinement Algebra
3 Properties of Iterations
4 Properties of fair
5 Properties of Fair and Concurrency
6 Properties of Fair Parallel
7 Conclusions
References
A Wide-Spectrum Language for Verification of Programs on Weak Memory Models
1 Introduction
2 Instruction Reordering in Weak Memory Models
2.1 Thread-Local Reorderings
2.2 Reordering and Forwarding Instructions
2.3 General Operational Rules for Reordering
2.4 Reasoning About Reorderings
3 Semantics
3.1 Formal Language
3.2 Operational Semantics
3.3 Reordering and Forwarding for ARM and POWER
4 Model Checking Concurrent Data Structures
4.1 Chase-Lev Deque
5 Related Work
6 Conclusion
References
Operational Semantics of a Weak Memory Model with Channel Synchronization
1 Introduction
2 Background
3 Abstract Syntax
4 Operational Semantics
4.1 Local States, Events, and Configurations
4.2 Reduction Steps
5 Strong Semantics
6 Relating the Strong and the Weak Semantics
6.1 The Strong Semantics Conditionally Simulates the Weak One
7 Related Work
8 Conclusion
References
Stepwise Development and Model Checking of a Distributed Interlocking System - Using RAISE
1 Introduction
1.1 Background
1.2 Contribution
1.3 Related Work
1.4 Paper Overview
2 Case Study
2.1 Engineering Concept
2.2 Overview of Formal Development
3 First Model
4 Second Model
5 Third Model
6 Verification
6.1 Model Checking
6.2 Other Verification Activities
7 Conclusion and Future Work
References
Resource-Aware Design for Reliable Autonomous Applications with Multiple Periods
1 Introduction
2 Related Work
3 The Motivating Example
4 Preliminaries
4.1 Atypical Task Graph
4.2 Communication Model
4.3 Active Redundancy Based Fault Tolerance
5 Reliable and Resource-Aware Design
5.1 Redundancy Optimization
5.2 Constraint Formalization and Resource Optimization
5.3 Implementation
6 Case Study
6.1 Redundancy Degree for Various Reliability Requirements
6.2 Resource Optimization Within Various Scenarios
6.3 Timing Constraint on Weak Dependency
7 Conclusion
References
Verifying Auto-generated C Code from Simulink
1 Introduction
2 The Case Studies
3 The BTC Tool
3.1 The BTC EmbeddedPlatform
4 Experience Report
4.1 Formalizing the Requirements
4.2 Formal Verification of Auto-generated Code
5 Reflections and Recommendations
5.1 Requirements
5.2 Code Verification
6 Conclusion
References
QFLan: A Tool for the Quantitative Analysis of Highly Reconfigurable Systems
1 Introduction
2 QFLan Architecture
3 QFLan at Work: Coffee Vending Machine
4 Outlook
References
Modular Verification of Programs with Effects and Effect Handlers in Coq
1 Introduction
2 Modelling Programs with Effects
2.1 Interface of Effects
2.2 Operational Semantics for Effects
2.3 The Program Monad
2.4 Components as Programs with Effects
3 Modular Verification of Programs with Effects
3.1 Definition
3.2 Compliance and Correctness
3.3 Proofs Techniques to Show Compliance for Components
4 Discussion
4.1 FreeSpec as a Methodology
4.2 FreeSpec as a Framework
5 Related Work
6 Conclusion and Future Work
References
Combining Tools for Optimization and Analysis of Floating-Point Computations
1 Introduction
2 Implementation
3 Experimental Results
4 Discussion
References
A Formally Verified Floating-Point Implementation of the Compact Position Reporting Algorithm
1 Introduction
2 The Compact Position Reporting Algorithm
2.1 Encoding
2.2 Local Decoding
2.3 Global Decoding
3 An Alternative Implementation of CPR
3.1 Alternative Encoding
3.2 Alternative Local Decoding
3.3 Alternative Global Decoding
4 Verification Approach
5 Related Work
6 Conclusion
References
Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations
1 Introduction
2 The Case Study
2.1 Controller Model
2.2 Simulink Design Verifier
2.3 Goals
3 Feasibility Analysis
3.1 Preparation
3.2 Verification
3.3 Scalability
4 Lessons Learned
4.1 Specification
4.2 Model
4.3 Verification Tool
5 Conclusions and Discussion
References
Multi-robot LTL Planning Under Uncertainty
1 Introduction
2 Running Example
3 Modeling Partial Knowledge in a Robotic Application
4 Planning with Partial Knowledge
5 Algorithms
6 Evaluation
7 Related Work
8 Conclusions
References
Vector Barrier Certificates and Comparison Systems
1 Introduction
2 Fundamental Definitions
2.1 Systems of Ordinary Differential Equations
2.2 Safety Verification and Direct Methods
3 Barrier Certificates
3.1 Comparison System-Based Barrier Certificates
3.2 Comparison Systems
3.3 Comparison Principle Interpretation of Barrier Certificates
3.4 Invariant Set-Based Barrier Certificates
4 From Scalar to Vector Comparison Systems
4.1 Vector Lyapunov Functions
4.2 Vector Comparison Principle
4.3 Safety with Vector Barrier Certificates
4.4 Generating Vector Barrier Certificates Using SDP
5 Limitations and Outlook
6 Related Work
7 Conclusion
References
Timed Vacuity
1 Introduction
2 Preliminaries
2.1 TCTL, Timed Automata, and Timed Transition Systems
2.2 Timed Vacuity
3 TCTL+ and Its Model Checking
4 Satisfying a TCTL Formula Timed Vacuously
4.1 Complexity Results
4.2 Algorithms for Tightening TCTL Formulas
5 Ranking Vacuity Results
6 Conclusions
References
Falsification of Cyber-Physical Systems Using Deep Reinforcement Learning
1 Introduction
2 Preliminary
3 Our Approach
3.1 Overview of Our Algorithm
3.2 Reward Definition for Life-Long Property Falsification
4 Preliminary Results
5 Conclusion and Future Work
References
Dynamic Symbolic Verification of MPI Programs
1 Introduction
2 Overview
3 MPI Model and Execution Semantics
4 Encoding Rules
5 Design
5.1 Components
5.2 Deadlock Detection
5.3 Correctness and Termination
6 Implementation
6.1 Non-chronological Backtracking
6.2 Terminated Interleavings
7 Evaluation
8 Related Work
9 Conclusion and Future Work
References
To Compose, or Not to Compose, That Is the Question: An Analysis of Compositional State Space Generation
1 Introduction
2 Related Work
3 Background
4 Methodology
5 Results
5.1 Case and Subject Descriptions
5.2 Analysis
5.3 Threats to Validity
6 Conclusions
References
View Abstraction for Systems with Component Identities
1 Introduction
1.1 Related Work
2 The Framework
2.1 Systems
3 Using View Abstraction
4 Bounding the Number of Components
5 Using Symmetry
6 The Algorithm and Implementation
6.1 Prototype Implementation
7 Analysing Reference-Linked Data Structures
8 Conclusions
References
Compositional Reasoning for Shared-Variable Concurrent Programs
1 Introduction
2 Related Work
3 Succinct Automata
3.1 Syntax and Semantics
3.2 Parallel Composition
4 Compositional Reasoning for Succinct Automata
4.1 Safety Verification of Succinct Automata
4.2 Simulations of Succinct Automata
4.3 Safety Property Preservation Under Refinement
5 Automatic Verification of Succinct Automata
5.1 Generation of Succinct Automata
5.2 Refinement Checking Between Succinct Automata
6 Conclusions and Future Work
References
Statistical Model Checking of LLVM Code
1 Introduction
2 Lodin
3 Plasma-Lab
4 Conclusion
References
SDN-Actors: Modeling and Verification of SDN Programs
1 Introduction
2 Overview
2.1 Concurrency Errors in SDN Networks
2.2 Actor-Based Modeling of SDN Networks
3 SDN-Actors: An Actor Based Encoding of SDN Programs
3.1 Network Topology
3.2 The Switch and Host Classes
3.3 The Controller
3.4 Barriers
4 DPOR-Based Model Checking of SDN-Actors
4.1 DPOR-Based Model Checking in Actors
4.2 Entry-Level and Context-Sensitive Independence
4.3 Comparison of DPOR Reductions with Related Work
5 Checking SDN Properties in Case Studies
6 Conclusions and Related Work
References
CompoSAT: Specification-Guided Coverage for Model Finding
1 Introduction
2 Motivation and Example
3 Adapting Coverage to Model Finding
4 Foundations
4.1 Bounded Model Finding
4.2 Local Necessity and Provenance
5 Algorithmics of Coverage
5.1 Expansion
5.2 Canonicalization
5.3 Coverage and Subsumption
6 Implementation
7 Qualitative Use Case: Overconstraint
7.1 Detecting Overconstraint via Local Necessity
7.2 Highlighting Uncovered Constraints
8 Evaluation
8.1 Experimental Setup
8.2 RQ1: Do Small Ensembles Suffice?
8.3 RQ2: Is Enumeration Effective?
8.4 RQ3: Minimal Model Coverage
9 Related Work
10 Conclusion and Discussion
References
Approximate Partial Order Reduction
1 Introduction
2 Preliminaries
2.1 Transition Systems
2.2 Discrepancy Functions
2.3 Combining Sets of Discrepancy Functions
3 Independent Actions and Neighboring Executions
3.1 Approximately Independent Actions
3.2 (,)-trace Equivalent Discrepancy for Action Pairs
4 Effect of -independent Traces
4.1 -equivalent Traces
4.2 (0,)-trace Equivalent Discrepancy for Traces (on the Same Initial States)
4.3 (,)-trace Equivalent Discrepancy for Traces
5 Reachability with Approximate Partial Order Reduction
5.1 Earliest Equivalent Position of an Action in a Trace
5.2 Reachability Using (,)-trace Equivalent Discrepancy
6 Experimental Evaluation of Effectiveness
7 Conclusion
References
A Lightweight Deadlock Analysis for Programs with Threads and Reentrant Locks
1 Introduction
2 Lams and the Algorithm for Detecting Circularities
3 The Language and Its Semantics
4 Static Semantics
5 Remarks About the Analysis Technique
6 Related Works and Conclusions
References
Formal Specification and Verification of Dynamic Parametrized Architectures
1 Introduction
2 Related Work
3 An Example of a Dynamic Parametrized Architecture
4 Formal Specification of Dynamic Parametrized Architectures
4.1 Definitions
4.2 Logic for Systems of Parameters
5 Analysis with SMT-Based Model Checking
5.1 Background Notions on SMT-Based Model Checking
5.2 Encoding into SMT-Based Model Checking
6 Experimental Evaluation
6.1 Setup
6.2 Benchmarks and Results
7 Conclusions and Future Work
References
FM 2018 Industry Day
From Formal Requirements to Highly Assured Software for Unmanned Aircraft Systems
1 Introduction
2 UAS Detect and Avoid
3 From DAIDALUS to ICAROUS
4 Conclusion
References
Interlocking Design Automation Using Prover Trident
Abstract
1 Background
2 The Prover Trident Process
2.1 PiSPEC IP
2.2 Prover iLock
2.3 Prover Certifier
3 Results and Conclusions
References
Model-Based Testing for Avionics Systems
1 Introduction
2 Core Challenges
2.1 Application Parameters
2.2 Interface Modules
2.3 Test Scenarios
3 Conclusion
References
On Software Safety, Security, and Abstract Interpretation
1 Introduction
2 Security in Safety-Critical Systems
3 Proving the Absence of Defects
4 Conclusion
References
Variant Analysis with QL
1 Introduction
2 QL for Ad-hoc Variant Analysis
3 Variant Analysis from Building Blocks
4 Conclusion
References
Object-Oriented Security Proofs
1 Security as Object Equivalence
2 Reasoning About Object Equivalence
3 Some Specification Examples
4 Conclusion
Z3 and SMT in Industrial R&D
1 Introduction
2 Driving Scenarios and Research Synergy
3 SMT-LIB - A Research Community
4 Tooling and Infrastructure
4.1 Development
4.2 Open Sourcing
5 Push, Pull and Confluences
References
Evidential and Continuous Integration of Software Verification Tools
1 Introduction
2 Verification Activities, Workflows and Patterns
3 Structure of the Integration Framework
4 Illustration
5 Conclusion
References
Disruptive Innovations for the Development and the Deployment of Fault-Free Software
1 Introduction
2 Software Modeling
3 Low Cost High Integrity Platform
4 Formal Data Validation
5 Conclusion and Perspectives
References
Author Index

Systemvoraussetzungen

Als PDF speichern Als Link merken