Integrated Formal Methods

Name: Integrated Formal Methods | 13th International Conference, IFM 2017, Turin, Italy, September 20-22, 2017, Proceedings
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

13th International Conference, IFM 2017, Turin, Italy, September 20-22, 2017, Proceedings

Nadia Polikarpova Steve Schneider(Herausgeber*in)

Springer (Verlag)

Erschienen am 11. September 2017

XXI, 438 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-319-66845-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
Invited Talks
Integrating Inference into Stochastic Process Algebra Models
Logic & Proofs for Cyber-Physical Systems with KeYmaera X
Machine Learning for Programming
Contents
Cyber-Physical Systems
An Active Learning Approach to the Falsification of Black Box Cyber-Physical Systems
1 Introduction
2 Background
2.1 Dynamical System
2.2 Signal Temporal Logic
2.3 Gaussian Processes
3 Domain Estimation with Gaussian Processes
4 The Falsification Process
4.1 Adaptive Optimization
5 Probabilistic Approximation Semantics
6 Case Studies and Results
7 Conclusions
References
Modelling and Verification of Timed Robotic Controllers
1 Introduction
2 Modelling Robotic Controllers
2.1 Motivating Example
2.2 Related Work
3 RoboChart: A Formal Notation for Robotics
4 Semantics
4.1 State Machines
4.2 Budgets and Deadlines
4.3 Clocks
5 Tool Support and Model-Checking
6 Conclusion
References
Spatial Reasoning About Motorway Traffic Safety with Isabelle/HOL
1 Introduction
2 Embedding MLSL into Isabelle/HOL
2.1 Semantic Model
2.2 Preliminary Definitions
2.3 Views
2.4 Traffic Snapshots
2.5 Sensors
2.6 Restriction to Views
2.7 Hybrid Multi-Lane Spatial Logic
3 Safety with Perfect Information
4 Safety with Regular Information
5 Conclusion
References
Formalising and Monitoring Traffic Rules for Autonomous Vehicles in Isabelle/HOL
1 Introduction
2 Preliminaries
3 Codification of Traffic Rules
3.1 Legal Analysis
3.2 LTL Formulas of Traffic Rules
3.3 Monitoring Traffic Rules
4 Concretising the Overtaking Predicate
4.1 Lanelets
4.2 Lane Detection
4.3 Overtaking Detection
5 Concretising the Safe Distance Predicate
6 Monitoring Overtaking Traffic Rules
7 Related Work and Conclusions
References
Software Verification Tools
Making Whiley Boogie!
1 Introduction
2 Background
2.1 Whiley
2.2 Boogie
3 Modeling Whiley in Boogie
3.1 Types
3.2 Control Flow
4 Generating Verification Conditions
5 Experimental Results
6 Related Work
7 Conclusion
References
Complexity Analysis for Java with AProVE
1 Introduction
2 Complexity of Java and Symbolic Execution Graphs
3 From SE Graphs to ITSs
4 Summarizing Method Calls
5 Encoding Heap Modifications
6 Experiments and Conclusion
References
The VerCors Tool Set: Verification of Parallel and Concurrent Software
1 Introduction
2 The VerCors Architecture
3 Verification Highlights
4 Conclusion and Related Work
References
An Extension of the ABS Toolchain with a Mechanism for Type Checking SPLs
1 Introduction
2 FDABS: A Minimal Language for Core ABS and Deltas
3 The Checking Mechanism for FDABS Product Lines
3.1 Unambiguity Checking
3.2 Type Checking Step (i): Extracting Constraints
3.3 Type Checking Step (ii): Building the PFGT
3.4 Type Checking Step (iii): Checking All Variants
4 Integration into the ABS Toolchain
4.1 An Overview of the Novel Component
4.2 On Building the PFGT
5 Case Studies and Evaluation
5.1 Error Reporting
5.2 Performance
5.3 Discussion
6 Related Work
7 Conclusion
References
Safety-Critical Systems
Generalised Test Tables: A Practical Specification Language for Reactive Systems
1 Introduction
2 The Basis: Concrete Test Tables
3 The Concept of Generalised Test Tables
4 Semantics of Generalised Test Tables
4.1 Unrolled Instances of Generalised Test Tables
4.2 Evaluation of Expressions
4.3 Two-Party Game for Defining Test Conformance
5 Transforming Generalised Test Tables into Automata
6 Experiment
7 Related Work
8 Conclusion
References
Transient and Steady-State Statistical Analysis for Discrete Event Simulators
1 Introduction
2 Batch Means Method
3 MultiVeStA
3.1 Simulator Integration
4 Analysis of a Biochemical Pathway Using MultiVeStA
4.1 Example 1: The cAMP/PKA/MAPK Biochemical Pathway
4.2 Transient Analysis with MultiVeStA
4.3 Steady-State Analysis in MultiVeStA
5 Example 2: Edinburgh Bus Simulator
6 Conclusions
References
Algebraic Compilation of Safety-Critical Java Bytecode
1 Introduction
2 Preliminaries
2.1 Safety-Critical Java
2.2 Circus
3 Our Approach to Algebraic Compilation
4 SCJVM and Interpreter Model
5 Shallow Embedding of C in Circus
6 Compilation Strategy
7 Discussion
8 Conclusions
References
Task-Node Mapping in an Arbitrary Computer Network Using SMT Solver
1 Introduction
1.1 ScOSA System Overview
1.2 Mapping and Subsequent Model Checking
2 Related Work
3 Formal Definition of the Problem
3.1 Period Estimation for Event-Triggered Tasks
3.2 Formulation of the Mapping Problem
4 SMT Formulation
4.1 Task-Node Mapping Variables
4.2 Link Bandwidth Constraints
4.3 Node Load Constraints
4.4 Objective Functions
4.5 Variable Types
5 Evaluation
5.1 Performance Comparison of Different SMT Formulations
5.2 Task-Node Mapping for the ATON Application
5.3 Remarks on Scalability
6 Conclusions and Future Work
References
Concurrency and Distributed Systems
Analysis of Synchronisations in Stateful Active Objects
1 Introduction
2 The Active Object Model gASP
3 Behavioural Type System
4 Behavioural Type Soundness and Analysis
5 Concluding Remarks
References
BTS: A Tool for Formal Component-Based Development
1 Introduction
2 CSP
3 BRIC
3.1 Component Contract
3.2 Component Instantiation
3.3 Composition Rules
3.4 Component Metadata
4 BRICK Tool Support
5 Evaluation
6 Conclusion
References
Testing and Verifying Chain Repair Methods for CORFU Using Stateless Model Checking
1 Introduction
2 Chain Replication
2.1 Basic Algorithm
2.2 Chain Repair
2.3 Chain Replication in CORFU
2.4 Chain Repair Techniques for CORFU
3 Stateless Model Checking, Erlang, Concuerror and Bounding
4 Modeling CORFU
4.1 Correctness Properties
4.2 Initial Model
4.3 Method 1: Add Repaired Server at End of Chain
4.4 Method 2: Add Repaired Server at Start of Chain
4.5 Method 3: Add Repaired Server in the Middle
4.6 An Evaluation of the Repair Methods on the Initial Model
5 Optimization and Refinements
5.1 Optimization: Avoid Reordering the Delivery of Unrelated Messages
5.2 Two Refinements of the Model
5.3 Evaluation of the Effect of the Optimization and Refinements
6 Related Work
7 Concluding Remarks
References
Synthesizing Coalitions for Multi-agent Games
1 Introduction
2 System Model
2.1 Motivating Example
2.2 Concurrent Game Graphs
3 TCLX
4 Expressiveness of TCLX
5 Satisfiability of TCLX
6 TCLX Model-Checking
7 Implementation and Experiments
8 Conclusion
References
Program Verification Techniques
Hoare-Style Reasoning from Multiple Contracts
1 Introduction
2 Reasoning About Multiple Contracts
2.1 Semantics
2.2 Normalization Rules
3 Derivation of General Reasoning Rules
3.1 Derivation of Three Instantiation Rules
3.2 Deriving the Elimination Rule
3.3 Deriving the Invariance Axiom and Rule
3.4 Deriving the Improved Adaptation Rule
3.5 Deriving the Generalized Adaptation Rule
3.6 Deriving the Conjunction Rule
4 Completeness
5 Related Work
6 Conclusions
References
A New Invariant Rule for the Analysis of Loops with Non-standard Control Flows
1 Introduction
2 Program Logic for Symbolic Execution
3 The Loop Invariant Rules
4 Evaluation
5 Exploiting Invariants: Integration of State Merging
6 Related Work
7 Future Work and Conclusion
References
Triggerless Happy
1 The Trouble with Triggers
2 Motivating Examples
3 Encoding Boogie in TPTP
3.1 Declarative Constructs
3.2 Imperative Constructs
4 Implementation and Experiments
4.1 Experimental Subjects
4.2 Experimental Setup
4.3 Experimental Results
5 Related Work
6 Discussion and Future Work
References
SemSlice: Exploiting Relational Verification for Automatic Program Slicing
1 Introduction
2 Background
2.1 Static Backward Slicing
2.2 Relational Program Verification
3 Implementation
4 Slice Candidate Generation
5 Evaluation
6 Related Work
7 Conclusion
References
Formal Modeling
VBPMN: Automated Verification of BPMN Processes (Tool Paper)
1 Introduction
2 Models and Languages
3 Web Application
4 CADP Back-End
5 Concluding Remarks
References
How Well Can I Secure My System?
1 Introduction
2 Security Modeling with Attack--defense Trees
2.1 Attack--defense Trees
2.2 Formal Semantics
3 Security-Oriented Optimization Problems
3.1 Mathematical Modeling
3.2 Implementation
3.3 Countermeasure Optimization on the Running Example
4 Conclusion
References
MaxUSE: A Tool for Finding Achievable Constraints and Conflicts for Inconsistent UML Class Diagrams
1 Introduction
2 Overall Architecture
3 Usage Scenarios
3.1 Verifying Consistency
3.2 Finding Achievable Constraints
3.3 Finding Constraint Conflicts
4 Usefulness
5 Availability
6 Related Work
7 Conclusion
References
Formal Verification of CNL Health Recommendations
1 Introduction
2 Background and Related Work
3 The Problem Domain and Framework
4 Controlled Natural Language for Therapy Algorithms
5 Case Frame Generation
6 Model Generation and Verification
6.1 Model Generation
6.2 Model Verification
7 Conclusion
References
Verified Software
Modular Verification of Order-Preserving Write-Back Caches
1 Introduction
2 Motivation
3 Components with Power Cuts
4 Crash-Safe Refinement
4.1 Data Refinement and Propagation of Jumps
4.2 Crash Refinement and Introduction of Jumps
5 Component Hierarchies and Substitution
6 Crash-neutrality
7 Related Work
8 Conclusion
References
Formal Verification of ARP (Address Resolution Protocol) Through SMT-Based Model Checking - A Case Study -
1 Introduction
2 Preliminaries on Formal Verification
3 Address Resolution Protocol (ARP)
3.1 ARP Formal Verification
4 Link-Local Addresses
4.1 Verification of ARP as in RFC 3927
5 Extended ARP: Address Conflict Detection
6 Conclusions
References
Certified Password Quality
1 Introduction
2 Password Quality Checking Software
3 Verified Password Quality in Coq
3.1 Types and Password Checkers
3.2 Specification, Implementation, and Proofs
3.3 Password Policies and Code Extraction
4 Evaluation
4.1 Experimental Setup
4.2 Experiment 1: Comparison with PAM Modules pam_cracklib and pam_pwdquality
4.3 Experiment 2: Increasing Password Entropy
4.4 Experiment 3: A Simple Policy
5 Related Work
6 Conclusion
References
Verification of STAR-Vote and Evaluation of FDR and ProVerif
1 Introduction
2 STAR-Vote in Communicating Sequential Processes and FDR
2.1 STAR-Vote CSP Model
2.2 Analysis with FDR
3 STAR-Vote in the Applied Pi Calculus and ProVerif
3.1 STAR-Vote Model in Applied Pi
3.2 Analysis with ProVerif
4 Evaluation of the Tools: FDR and ProVerif
4.1 Expressiveness
4.2 Usability
4.3 Efficiency
5 Related Work
6 Conclusion
References
Author Index

Systemvoraussetzungen

Als PDF speichern Als Link merken