Critical Systems: Formal Methods and Automated Verification: Joint 21st International Workshop on Formal Methods for Industrial Critical Systems and 16th International Workshop on Automated Verification of Critical Systems, FMICS-AVoCS 2016, Pisa, Italy, September 26-28, 2016, Proceedings

✍ Scribed by Maurice H. ter Beek, Stefania Gnesi, Alexander Knapp (eds.)

• Publisher: Springer International Publishing
• Year: 2016
• Tongue: English
• Leaves: 255
• Series: Lecture Notes in Computer Science 9933
• Edition: 1
• Category: Library

✦ Synopsis

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.

✦ Table of Contents

Front Matter....Pages I-XVI
Front Matter....Pages 1-1
Model-Based Testing Strategies and Their (In)dependence on Syntactic Model Representations....Pages 3-21
Front Matter....Pages 23-23
Abstract Interpretation of MATLAB Code with Interval Sets....Pages 25-38
Workflow Nets Verification: SMT or CLP?....Pages 39-55
One Step Towards Automatic Inference of Formal Specifications Using Automated VeriFast....Pages 56-64
Analyzing Unsatisfiability in Bounded Model Checking Using Max-SMT and Dual Slicing....Pages 65-80
Towards the Automated Verification of Weibull Distributions for System Failure Rates....Pages 81-96
Fault-Aware Modeling and Specification for Efficient Formal Safety Analysis....Pages 97-114
Front Matter....Pages 115-115
Block Library Driven Translation Validation for Dataflow Models in Safety Critical Systems....Pages 117-132
A Model-Based Framework for the Specification and Analysis of Hierarchical Scheduling Systems....Pages 133-141
Utilising ({\mathbb {K}}) Semantics for Collusion Detection in Android Applications....Pages 142-149
Unified Simulation, Visualization, and Formal Analysis of Safety-Critical Systems with ....Pages 150-167
Front Matter....Pages 169-169
Formal Verification of a Rover Anti-collision System....Pages 171-188
Verification of AUTOSAR Software Architectures with Timed Automata....Pages 189-204
Verification by Way of Refinement: A Case Study in the Use of Coq and TLA in the Design of a Safety Critical System....Pages 205-213
Application of Coloured Petri Nets in Modelling and Simulating a Railway Signalling System....Pages 214-230
Formal Techniques for a Data-Driven Certification of Advanced Railway Signalling Systems....Pages 231-245
Back Matter....Pages 247-247

✦ Subjects

Logics and Meanings of Programs;Programming Languages, Compilers, Interpreters;Software Engineering;Special Purpose and Application-Based Systems;Mathematical Logic and Formal Languages