Servicenavigation

Detailseite

Zurück

Projekt Druckansicht

Directed Model Checking in the Analysis of Real-Time and Probabilistic Systems

Fachliche Zuordnung Softwaretechnik und Programmiersprachen
Förderung Förderung von 2005 bis 2009
Projektkennung Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 5454936
 
Erstellungsjahr 2019

Zusammenfassung der Projektergebnisse

The proper functioning of embedded and cyber-physical systems is an essential objective in software and systems engineering. This is particularly true when those systems are safety-critical, which means that their malfunctioning may endanger the environment or human life. The design process relies on the specification of essential system properties, followed by an architectural design in which the functioning of different system components is developed. An essential system property could be, for instance, that an air bag in a car will not explode unless an accident actually has been detected. For many of these systems it is essential that they satisfy what is referred to as ”non-functional” system properties. Those are properties that rely, for instance, on real time bounds, such as ”the air bag shall be deployed no later than 50 ms after the detection of a crash”. Since many safety-critical systems are not entirely safe, what is often required are probabilistic timed guarantees, such as ”the probability of the airbag being deployed even if no crash has been detected is smaller than 10^−9 per hour of operation.” As a consequence, the focus of the work in this research project has been on developing automated verification technology which checks whether such probabilistic timed properties are actually guaranteed by the architectural design of the model. The technology that we develop is based on model checking, which is a complete and terminating procedure inspecting all possible configurations, here called states, of the system. It is automatic because once the specification is formulated and the architectural design is modeled, the procedure executes without any further user interaction. This makes model checking based technology a prime candidate for inclusion into practical system design processes. While the model checking technology for those types of properties is well developed, we identified in the beginning of the project a dearth in computing explanations for the reason of a property violation. A probabilistic model checker will tell the user whether a property is valid or violated, but not provide an explanation why a violation occurs. The approach that we have developed in this project computes such explanations, which we refer to as counterexamples. They represent a set of executions of the system that start in its initial state and end in a state where the property is violated, e.g., where the airbag has been exploded without a crash having been detected beforehand. Since we are considering probabilistic properties, each such trace carries a probability of occurrence. Obviously, it is desirable to include those system traces into the counterexample for which the probability is highest, so that we obtain a good number of meaningful and very probable property violating traces in the counterexample. In order to achieve this goal we are using heuristics guided search algorithms, gleaned from the area of Artificial Intelligence, in computing the counterexample. The Algorithms that we consider are Best-First Search, Z* and A*. In particular, we consider the counterexample computation problem as an instance of the k-shortest-paths (KSP) problem. To solve this problem, we developed the K* algorithm, which is first and, at the time of writing, only heuristics guided, on-the-fly algorithm to solve the KSP problem. In addition to being very useful in the computation of counterexamples, it has many applications in other domains, for instance in route planning. In order to establish the applicability to real-life engineering problems we have applied this counterexample computation to an analysis of the architecture of an industrial air bag system architecture. Using the counterxample computation we could prove that for this example, using just one microprocessor for the signal processing would not suffice to achieve a legally required system dependability and that, hence, a second redundant microprocessor needed to be added. In subsequent research we have extended this approach to a comprehensive probabilistic safety analysis method leading to the automatic synthesis of probabilistic fault trees, a common engineering safety analysis notation.

Projektbezogene Publikationen (Auswahl)

 
 

Zusatzinformationen

© 2024 DFG Kontakt / Impressum / Datenschutz

Textvergrößerung und Kontrastanpassung