Critical Systems: Formal Methods and Automated Verification

1. Front Matter

   Pages I-XVI

   PDF

2. Invited Talk

   1. Front Matter

      Pages 1-1

      PDF

   2. Model-Based Testing Strategies and Their (In)dependence on Syntactic Model Representations

      • Jan Peleska, Wen-ling Huang

      Pages 3-21

3. Automated Verification Techniques

   1. Front Matter

      Pages 23-23

      PDF

   2. Abstract Interpretation of MATLAB Code with Interval Sets

      • Christian Dernehl, Norman Hansen, Stefan Kowalewski

      Pages 25-38

   3. Workflow Nets Verification: SMT or CLP?

      • Hadrien Bride, Olga Kouchnarenko, Fabien Peureux, Guillaume Voiron

      Pages 39-55

   4. One Step Towards Automatic Inference of Formal Specifications Using Automated VeriFast

      • Mahmoud Mohsen, Bart Jacobs

      Pages 56-64

   5. Analyzing Unsatisfiability in Bounded Model Checking Using Max-SMT and Dual Slicing

      • Takuro Kutsuna, Yoshinao Ishii

      Pages 65-80

   6. Towards the Automated Verification of Weibull Distributions for System Failure Rates

      • Yu Lu, Alice A. Miller, Ruth Hoffmann, Christopher W. Johnson

      Pages 81-96

   7. Fault-Aware Modeling and Specification for Efficient Formal Safety Analysis

      • Axel Habermaier, Alexander Knapp, Johannes Leupolz, Wolfgang Reif

      Pages 97-114

4. Model-Based System Analysis

   1. Front Matter

      Pages 115-115

      PDF

   2. Block Library Driven Translation Validation for Dataflow Models in Safety Critical Systems

      • Arnaud Dieumegard, Andres Toom, Marc Pantel

      Pages 117-132

   3. A Model-Based Framework for the Specification and Analysis of Hierarchical Scheduling Systems

      • Mounir Chadli, Jin Hyun Kim, Axel Legay, Louis-Marie Traonouez, Stefan Naujokat, Bernhard Steffen et al.

      Pages 133-141

   4. Utilising \({\mathbb {K}}\) Semantics for Collusion Detection in Android Applications

      • Irina Măriuca Asăvoae, Hoang Nga Nguyen, Markus Roggenbach, Siraj Shaikh

      Pages 142-149

   5. Unified Simulation, Visualization, and Formal Analysis of Safety-Critical Systems with

      • Axel Habermaier, Johannes Leupolz, Wolfgang Reif

      Pages 150-167

5. Applications and Case Studies

   1. Front Matter

      Pages 169-169

      PDF

   2. Formal Verification of a Rover Anti-collision System

      • Ning Ge, Eric Jenn, Nicolas Breton, Yoann Fonteneau

      Pages 171-188

   3. Verification of AUTOSAR Software Architectures with Timed Automata

      • Steffen Beringer, Heike Wehrheim

      Pages 189-204

   4. Verification by Way of Refinement: A Case Study in the Use of Coq and TLA in the Design of a Safety Critical System

      • Philip Johnson-Freyd, Geoffrey C. Hulette, Zena M. Ariola

      Pages 205-213

   5. Application of Coloured Petri Nets in Modelling and Simulating a Railway Signalling System

      • Somsak Vanit-Anunchai

      Pages 214-230

This book constitutes the refereed proceedings of the Joint 21st International Workshop on Formal Methods for Industrial Critical Systems and the 16th International Workshop on Automated Verification of Critical Systems, FMICS-AVoCS 2016, held in Pisa, Italy, in September 2016.
The 11 full papers and 4 short papers presented together with one invited talk were carefully reviewed and selected from 24 submissions. They are organized in the following sections: automated verification techniques; model-based system analysis; and applications and case studies.

• dynamic analysis
• formal methods
• logic and verification
• model checking
• software testing and debugging
• automata theory
• Gaussian processes
• grammars and context-free languages
• linear type-systems
• monitorability
• monitoring algorithms
• quantitative semantics
• regular languages
• runtime adaptation
• software verification
• spatio-temporal logic
• transducers
• Turing patterns
• uncertainty
• weighted graphs

• ISTI-CNR , Pisa, Italy

  Maurice H. ter Beek, Stefania Gnesi

• Universität Augsburg, Augsburg, Germany

  Alexander Knapp

Policies and ethics