Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
ATZ-Fachkongress

Chassis.tech plus 2024


4 Kongresse in einer Veranstaltung

Treffen Sie in München die Fachleute von Chassis, Lenkung, Bremsen sowie Reifen/Räder.
Erweiterte Suche
Anmelden
nach oben

2022 | Buch

Reinforcement Learning with Guarantees that Hold for Ever Kapitel lesen Erstes Kapitel lesen

Formal Methods for Industrial Critical Systems

27th International Conference, FMICS 2022, Warsaw, Poland, September 14–15, 2022, Proceedings

herausgegeben von: Prof. Jan Friso Groote, Prof. Dr. Marieke Huisman

Verlag: Springer International Publishing

Buchreihe : Lecture Notes in Computer Science

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten
insite
SUCHEN

Über dieses Buch

This book constitutes the proceedings of the 27th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2022, which took place in Warsaw, Poland, in September 2022. The 13 full papers included in this book were carefully reviewed and selected from 22 submissions. They were organized in topical sections as follows: Certification; industrial use cases; testing and monitoring; and methodology.

Inhaltsverzeichnis

Frontmatter

Invited Keynote Talks

Frontmatter
Reinforcement Learning with Guarantees that Hold for Ever
Abstract
Reinforcement learning is a successful explore-and-exploit approach, where a controller tries to learn how to navigate an unknown environment. The principle approach is for an intelligent agent to learn how to maximise expected rewards. But what happens if the objective refers to non-terminating systems? We can obviously not wait until an infinite amount of time has passed, assess the success, and update. But what can we do? This talk will tell.
Ernst Moritz Hahn, Mateo Perez, Sven Schewe, Fabio Somenzi, Ashutosh Trivedi, Dominik Wojtczak
Supporting Railway Innovations with Formal Modelling and Verification
Abstract
It is a continuing challenge for European railway infrastructure managers to increase the capacity of the dense European railway network and to achieve cost reductions at the same time. Innovations developed to that effect rely heavily on digital technology. To cope with the ensued complexity, railway infrastructure managers are starting to appreciate more and more the use of formal modelling and verification techniques to support the development of these digital innovations. In my presentation I will discuss our contributions to two ongoing innovations in the railway domain: EULYNX and ERTMS/ETCS Hybrid Level 3.
Bas Luttik

Certification

Frontmatter
Formal Monotony Analysis of Neural Networks with Mixed Inputs: An Asset for Certification
Abstract
The use of ML technology to design safety-critical systems requires a complete understanding of the neural network’s properties. Among the relevant properties in an industrial context, the verification of partial monotony may become mandatory. This paper proposes a method to evaluate the monotony property using a Mixed Integer Linear Programming (MILP) solver. Contrary to the existing literature, this monotony analysis provides a lower and upper bound of the space volume where the property does not hold, that we denote “Non-Monotonic Space Coverage”. This work has several advantages: (i) our formulation of the monotony property works on discrete inputs, (ii) the iterative nature of our algorithm allows for refining the analysis as needed, and (iii) from an industrial point of view, the results of this evaluation are valuable to the aeronautical domain where it can support the certification demonstration. We applied this method to an avionic case study (braking distance estimation using a neural network) where the verification of the monotony property is of paramount interest from a safety perspective.
Guillaume Vidot, Mélanie Ducoffe, Christophe Gabreau, Ileana Ober, Iulian Ober
Generating Domain-Specific Interactive Validation Documents
Abstract
In state-of-the-art approaches, requirements are gradually encoded into the model, with each modeling step being verified. Once the modeling and verification process has finished, code generation is usually applied to generate the final product. Finally, the generated code is validated, e.g., by executing tests, or running simulations. At this point, stakeholders and domain experts are actively incorporated into the development process. Especially in industrial applications, validation is as important as verification. Thus, it is important to integrate the stakeholders’ and the domain experts’ feedback as early as possible. In this work, we propose two approaches to tackle this: (1) a static export of an animation trace into a single HTML file, and (2) a dynamic export of a classical B model to an interactive HTML document, both with a domain-specific visualization. For the second approach, we extend the high-level code generator B2Program by JavaScript, and integrate VisB visualizations. An important aspect here is to ease communication between modelers and domain experts, which is achieved by implementing features to share animated traces, and giving feedback to each other.
Fabian Vu, Christopher Happe, Michael Leuschel
Deductive Verification of Smart Contracts with Dafny
Abstract
We present a methodology to develop verified smart contracts. We write smart contracts, their specifications and implementations in the verification-friendly language Dafny. In our methodology the ability to write specifications, implementations and to reason about correctness is a primary concern. We propose a simple, concise yet powerful solution to reasoning about contracts that have external calls. This includes arbitrary re-entrancy which is a major source of bugs and attacks in smart contracts. Although we do not yet have a compiler from Dafny to EVM bytecode, the results we obtain on the Dafny code can reasonably be assumed to hold on Solidity code: the translation of the Dafny code to Solidity is straightforward. As a result our approach can readily be used to develop and deploy safer contracts.
Franck Cassez, Joanne Fuller, Horacio Mijail Antón Quiles

Industrial Use Cases

Frontmatter
Towards Reusable Formal Models for Custom Real-Time Operating Systems
Abstract
In embedded systems, the execution semantics of the real-time operating system (RTOS), which is responsible for scheduling and timely execution of concurrent processes, is crucial for the correctness of the overall system. However, existing approaches for the formal verification of embedded systems typically abstract from the RTOS completely, or provide a detailed and synthesizable formal model of the RTOS. While the former may lead to unsafe systems, the latter is not compatible with industrial design processes. In this paper, we present an approach for reusable abstract formal models that can be configured for custom RTOS. Our key idea is to formally capture common execution mechanisms of RTOS like preemptive scheduling and event synchronization abstractly in configurable timed automata models. These abstract formal models can be configured for a concrete custom RTOS, and they can be combined into a formal system model together with a concrete application. Our reusable models significantly reduce the manual effort of defining a formal model that captures concurrency and real-time behavior together with the functionality of an application. The resulting formal model enables analysis, verification, and graphical simulation. We validate our approach by formalizing and analyzing a rescue robot application running the custom open source RTOS EV3RT.
Julius Adelt, Julian Gebker, Paula Herber
Formal Verification of an Industrial UML-like Model using mCRL2
Abstract
Low-code development platforms are gaining popularity. Essentially, such platforms allow to shift from coding to graphical modeling, helping to improve quality and reduce development time. The Cordis SUITE is a low-code development platform that adopts the Unified Modeling Language (UML) to design complex machine-control applications. In this paper we introduce Cordis models and their semantics. To enable formal verification, we define an automatic translation of Cordis models to the process algebraic specification language mCRL2. As a proof of concept, we describe requirements of the control software of an industrial cylinder model developed by Cordis, and show how these can be verified using model checking. We show that our verification approach is effective to uncover subtle issues in the industrial model and its implementation.
Anna Stramaglia, Jeroen J. A. Keiren
Chemical Case Studies in KeYmaera X
Abstract
Safety-critical chemical processes are well-studied in the formal methods literature, including hybrid systems models which combine discrete and continuous dynamics. This paper is the first to use a theorem-prover to verify hybrid chemical models: the KeYmaera X prover for differential dynamic logic. KeYmaera X provides parametric results that hold for a whole range of parameter values, non-linear physical dynamics, and a small trusted computing base.
We tell a general story about KeYmaera X: recent advances in automated reasoning about safety and liveness for differential equations have enabled elegant proofs about reaction dynamics.
Rose Bohrer
Analysing Capacity Bottlenecks in Rail Infrastructure by Episode Mining
Abstract
We introduce a methodology to identify and analyse capacity bottlenecks in railway networks. It is based on operational data that has been recorded in real operation. In a first step, network areas that exhibit frequent and significant train delays are determined. Next, the actual causes of such delays are investigated by analysing interdependences between train runs and by distinguishing between primary and secondary delays. This is achieved by employing episode mining techniques to enable the systematic identification of temporal patterns that occur frequently in the data about train runs.
Philipp Berger, Wiebke Lenze, Thomas Noll, Simon Schotten, Thorsten Büker, Mario Fietze, Bastian Kogel

Testing and Monitoring

Frontmatter
Test Suite Augmentation for Reconfigurable PLC Software in the Internet of Production
Abstract
Regression testing is an established technique used to attest the correctness of reconfigurations to PLC software. After such a reconfiguration, a test suite might not be adequate to ensure the absence of regressions, requiring the derivation of new test cases to uncover potential regressions. This paper presents a combination of state-of-the-art symbolic execution algorithms for test suite augmentation, an indispensable part of regression testing. Test generation is guided towards the changed behavior using a technique known as four-way forking. The old and new PLC software are executed in the same symbolic execution instance to account for the effects of the reconfiguration and increase the chances of generating difference-revealing test cases. The prototypical implementation is evaluated using domain-specific benchmarks such as the PLCopen Safety library and the Pick and Place Unit, exposing the limitations in applicability and effectiveness of the used techniques for safeguarding PLC software subject to frequent reconfigurations as found in cyber-physical production systems.
Marco Grochowski, Marcus Völker, Stefan Kowalewski
Monitoring of Spatio-Temporal Properties with Nonlinear SAT Solvers
Abstract
The automotive industry is increasingly dependent on computing systems with variable levels of critical requirements. The verification and validation methods for these systems are now leveraging complex AI methods, for which the decision algorithms introduce non-determinism, especially in autonomous driving. This paper presents a runtime verification technique agnostic to the target system, which focuses on monitoring spatio-temporal properties that abstract the evolution of objects’ behavior in their spatial and temporal flow. First, a formalization of three known traffic rules (from the Vienna convention on road traffic) is presented, where a spatio-temporal logic fragment is used. Then, these logical expressions are translated to a monitoring model written in the first-order logic, where they will be processed by a non-linear satisfiability solver. Finally, the translation allows the solver to check the validity of the encoded properties according to an instance of a specific traffic scenario (a trace). The results obtained from our tool that automatically generates a monitor from a formula show that our approach is feasible for online monitoring in a real-world environment.
André de Matos Pedro, Tomás Silva, Tiago Sequeira, João Lourenço, João Costa Seco, Carla Ferreira
Model-Based Testing of Internet of Things Protocols
Abstract
Internet of Things (IoT) is a popular term to describe systems/devices that connect and interact with each other through a network, e.g., the Internet. These devices communicate with each other via a communication protocol, such as Zigbee or Bluetooth Low Energy (BLE), the subject of this paper. Communication protocols are notoriously hard to implement correctly and a large set of test-cases is needed to check for conformance to the standard. Many of us have encountered communication problems in practice, such as random mobile phone disconnects, difficulty obtaining a Bluetooth connection, etc. In this paper, we research the application of industry strength Model-Based Testing (MBT) within the IoT domain. This technique contributes to higher quality specifications and more efficient and more thorough conformance testing. We show how we can model part of the BLE protocol specification using the Axini Modeling Platform (AMP). Based on the model, AMP is then able to automatically test the conformance of a BLE device. With this approach, we found specification flaws in the official BLE specifications as well as conformance errors on a certified BLE system.
Xavier Manuel van Dommelen, Machiel van der Bijl, Andy Pimentel

Methodology

Frontmatter
Formally Verifying Decompositions of Stochastic Specifications
Abstract
According to the principles of compositional verification, verifying that lower-level components satisfy their specification will ensure that the whole system satisfies its top-level specification. The key step is to ensure that the lower-level specifications constitute a correct decomposition of the top-level specification. In a non-stochastic context, such decomposition can be analyzed using techniques of theorem proving. In industrial applications, especially for safety-critical systems, specifications are often of stochastic nature, for example giving a bound on the probability that system failure will occur before a given time. A decomposition of such a specification requires techniques beyond traditional theorem proving. The first contribution of the paper is a theoretical framework that allows the representation of, and reasoning about, stochastic and timed behavior of systems as well as specifications for such behaviors. The framework is based on traces that describe the continuous-time evolution of a system, and specifications are formulated using timed automata combined with probabilistic acceptance conditions. The second contribution is a novel approach to verifying decomposition of such specifications by reducing the problem to checking emptiness of the solution space for a system of linear inequalities.
Anton Hampus, Mattias Nyberg
Verification of Behavior Trees using Linear Constrained Horn Clauses
Abstract
In the field of industrial production the usage of Behavior Trees sparks interest due to their modularity and flexibility. Considering Behavior Trees are used in a safety-critical domain, there is increased interest for methods to verify a Behavior Tree’s safety. Current approaches for Behavior Trees are only semi-automatic since they require manually added low-level details about the action’s behavior.
In this paper, we describe an automatic verification method for safety properties on Behavior Trees using Linear Constrained Horn Clauses (LCHCs). Our approach encodes all components of the verification task as CHCs, that is, the structure and semantics of the Behavior Tree, the implemented actions in the leaf nodes and the safety property itself. These clauses are then solved by a state-of-the-art SMT solver, leading to an efficient algorithm for Behavior Tree verification, which we evaluate by comparing our method against a general purpose verification framework.
Thomas Henn, Marcus Völker, Stefan Kowalewski, Minh Trinh, Oliver Petrovic, Christian Brecher
A Multi-level Methodology for Behavioral Comparison of Software-Intensive Systems
Abstract
Software-intensive systems constantly evolve. To prevent software changes from unintentionally introducing costly system defects, it is important to understand their impact to reduce risk. However, it is in practice nearly impossible to foresee the full impact of software changes when dealing with huge industrial systems with many configurations and usage scenarios. To assist developers with change impact analysis we introduce a novel multi-level methodology for behavioral comparison of software-intensive systems. Our fully automated methodology is based on comparing state machine models of software behavior. We combine existing complementary comparison methods into a novel approach, guiding users step by step through relevant differences by gradually zooming in on more and more details. We empirically evaluate our work through a qualitative exploratory field study, showing its practical value using multiple case studies at ASML, a leading company in developing lithography systems. Our method shows great potential for preventing regressions in system behavior for software changes.
Dennis Hendriks, Arjan van der Meer, Wytse Oortwijn
Backmatter
Metadaten
Titel
Formal Methods for Industrial Critical Systems
herausgegeben von
Prof. Jan Friso Groote
Prof. Dr. Marieke Huisman
Copyright-Jahr
2022
Electronic ISBN
978-3-031-15008-1
Print ISBN
978-3-031-15007-4
DOI
https://doi.org/10.1007/978-3-031-15008-1

Premium Partner

    Bildnachweise