Formal Methods For Industrial Critical Systems: 23rd International Conference, Fmics 2018, Maynooth, Ireland, September 3-4, 2018, Proceedings (lecture Notes In Computer Science)

This book constitutes the proceedings of the 23rd International Conference on Formal Methods for Industrial Critical Systems, FMICS 2018, held in Maynooth, Ireland, in September 2018. The 9 regular papers presented in this volume were carefully reviewed and selected from 17 submissions. The book also contains two invited talks in full-paper length. In addition, there are 8 invited contributions in honor of Susanne Graf (Director of Research at VERIMAG Grenoble, France) on the occasion of her 60 th birthday. The aim of the FMICS conference series is to provide a forum for researchers who are interested in the development and application of formal methods in industry. In particular, FMICS brings together scientists and engineers who are active in the area of formal methods and interested in exchanging their experiences in the industrial usage of these methods. The FMICS conference series also strives to promote research and development for the improvement of formal methods and tools for industrial applications. Front Matter ....Pages I-XVI Front Matter ....Pages 1-1 Generative Model Driven Design for Agile System Design and Evolution: A Tale of Two Worlds (Tiziana Margaria)....Pages 3-18 Building Correct Cyber-Physical Systems: Why We Need a Multiview Contract Theory (Susanne Graf, Sophie Quinton, Alain Girault, Gregor Gössler)....Pages 19-31 Front Matter ....Pages 33-33 Automated Functional Safety Analysis of Automated Driving Systems (Martin Kölbl, Stefan Leue)....Pages 35-51 Safety Interlocking as a Distributed Mutual Exclusion Problem (Alessandro Fantechi, Anne E. Haxthausen)....Pages 52-66 Checking Consistency of Real-Time Requirements on Distributed Automotive Control Software Early in the Development Process Using UPPAAL (Jan Toennemann, Andreas Rausch, Falk Howar, Benjamin Cool)....Pages 67-82 Formal Verification of a Programmable Hypersurface (Panagiotis Kouvaros, Dimitrios Kouzapas, Anna Philippou, Julius Georgiou, Loukas Petrou, Andreas Pitsillides)....Pages 83-97 Modelling and Analysing ERTMS Hybrid Level 3 with the mCRL2 Toolset (Maarten Bartholomeus, Bas Luttik, Tim Willemse)....Pages 98-114 Progress Checking for Dummies (Antti Valmari, Henri Hansen)....Pages 115-130 Virtual Integration for Pattern-Based Contracts with the Kind2 Model Checker (Jan Steffen Becker)....Pages 131-146 Active Mining of Document Type Definitions (Markus Frohme, Bernhard Steffen)....Pages 147-161 Adaptive Learning for Learn-Based Regression Testing (David Huistra, Jeroen Meijer, Jaco van de Pol)....Pages 162-177 Front Matter ....Pages 179-180 Predicate Abstraction and Such... (Bernhard Steffen, Tiziana Margaria)....Pages 181-188 Compositional Verification in Action (Hubert Garavel, Frédéric Lang, Laurent Mounier)....Pages 189-210 A Note on Refinement in Hierarchical Transition Systems (Gerald Lüttgen)....Pages 211-222 M3C: Modal Meta Model Checking (Bernhard Steffen, Alnis Murtovi)....Pages 223-241 Wholly!: A Build System For The Modern Software Stack (Loic Gelle, Hassen Saidi, Ashish Gehani)....Pages 242-257 A Modeling Language for Security Threats of IoT Systems (Delphine Beaulaton, Ioana Cristescu, Axel Legay, Jean Quilbeuf)....Pages 258-268 Revisiting Bounded Reachability Analysis of Timed Automata Based on MILP (Iulian Ober)....Pages 269-283 Evaluation and Comparison of Real-Time Systems Analysis Methods and Tools (Sophie Quinton)....Pages 284-290 Back Matter ....Pages 291-291 This Festschrift is published in honor of Kim Guldstrand Larsen, one of the earliest precursors of computer science in Denmark, on the occasion of his 60th birthday. During the last three decades, Kim Guldstrand Larsen has given major contributions across a remarkably wide range of topics, including real-time, concurrent, and probabilistic models of computation, logic in computer science, and model checking. Since 1995, he has been one of the prime movers behind the model checking tool for real-time systems UPPAAL, for which he was a co-recipient of the CAV Award in 2013. The Festschrift contains 32 papers that feature the broad range of Kim Guldstrand Larsen's research topics, such as formal languages and automata theory; logic; verification, model checking and testing; algorithmic game theory and mechanism design; semantics and reasoning; real-time and distributed systems; and modeling and simulation. This volume has been prepared in honor of Prof. Georg Färber, to celebrate his 34 years of service at TU München, as the Head of the Lehrstuhl für Realzeit-Computersysteme.It contains a collection of articles reflecting the state-of-the-art in the area of real-time systems. The topics included span over automotive software and electronics, software timing analysis, models for real-time systems, compilation of real-time programs, real-time microkernels and cyber-physical systems. It is intended to serve as a reference book for graduate-level courses. It will also be helpful to both researchers in the academia, as well as to practitioners from the industry This volume contains the lectures given in honor to Georg Färber as tribute to his contributions in the area of real-time and embedded systems. The chapters of many leading scientists cover a wide range of aspects, like robot or automotive vision systems or medical aspects. This volume contains the lectures given in honor to Georg Farber as tribute to his contributions in the area of real-time and embedded systems. The chapters of many leading scientists cover a wide range of aspects, like robot or automotive vision systems or medical aspects.