Unvollständige automatische Verifikation von Software-Designmodellen für nebenläufige objektorientierte eingebettete Echtzeitsysteme basierend auf dem Paradigma der erweiterten kommunizierenden Zustandsautomaten.
Zusammenfassung der Projektergebnisse
Models based on the Communicating Finite State Machine (CFSM) paradigm are frequently the foundation of design languages, methodologies and tools that are used in software and systems engineering practice. In order to build dependable software systems, in particular critical cyber-physical systems, it is essential to assert the safety and correctness of the design of these systems as early on in the life-cycle as possible. A prominent design language for cyber-physical systems is the family of Unified Modeling Language (UML)- type languages, such as the UML-RT language. UML-RT is a largely graphical modeling language and is based on a CFSM model. There are interesting properties of CFSM models, such as whether there is a maximum filling of individual buffers or whether there are looping executions during which no visible progress is made (livelocks), that are undecidable. This means that there can be no algorithm that decides whether these properties are satisfied in the general case. This does, however, not mean that certain, and possibly even a large number of, problem instances could not be decided. We have developed so-called semi-tests for these properties of CFSMs based on a translation to the solvability property of linear equation systems. We have successfully applied this technique to case studies of industrial size, amongst them the GARP protocol that is used in an Ethernet LAN. In order to perform proof-based verification of CFSM models we have developed a method to derive invariants, those are local properties that will not be violated by any compuation step of the system, for message queues. These invariants will help in conducting automated correctness proofs for CFSM models, in particular to show non-termination of a model or program involving queue based communication. Analyzing a UML-type model requires understanding its meaning in terms of the sequences of computation steps that it represents. Since language standards as well as tool vendors often describe and interpret this semantics in different ways, we have developed a framework for describing the semantics of the UML- RT language. Our semantic interpretation method translates UML-RT models into Abstract State Machines, a language frequently used to describe program semantics, and encompasses variation points in order to account for the different semantic interpretations of the UML-RT notation. This work includes an analysis of the UML-RT semantics implemented in the IBM Rational Rose RT tool that is frequently used in industrial practice. When analyzing properties of CFSM models using finite state verification technology, such as model checking, the tool returns diagnostic traces that represent computations of the system leading into a property violating state. These traces are often referred to as counterexamples. They are provided with the goal of debugging the CFSM model. However, these counterexamples can be very long, and there can be many of them, hence their direct inspection hardly ever pinpoints the very cause for the property violation. We have therefore developed the idea of contrast pattern mining, based on sequential pattern mining, which is a data mining technique for instance used in shopping basket analysis. The idea is to mine patterns of a few events or computation steps occurring along the good and the bad traces in a system that are frequently occurring in the bad traces, i.e., the ones violating a desired property, but infrequently in the good traces. We have applied this to CFSM models given in the Promela language and have obtained promising results, even though there remain some scalability issues to be resolved. Notice that UML-type CFSM models can be translated into Promela. In conclusion, we have made significant contributions to the very relevant but at the same time also very broad problem of asserting properties of CFSM-based UML-type software and system design models. Current work at the Chair for Software and Systems Engineering of the University of Konstanz centers around automated dependability and safety analysis of models of critical cyber-physical systems. It greatly benefits from insights gained in the course of the IMCOS project.
Projektbezogene Publikationen (Auswahl)
-
An asml semantics for dynamic structures and run time schedulability in UML-RT. In Richard F. Paige and Bertrand Meyer, editors, Objects, Components, Models and Patterns, 46th International Conference, TOOLS EUROPE 2008, Zurich, Switzerland, June 30 - July 4, 2008. Proceedings, volume 11 of Lecture Notes in Business Information Processing, pages 238–257. Springer, 2008
Stefan Leue, Alin Stefanescu, and Wei Wei
-
Dependency analysis for control flow cycles in reactive communicating processes. In Klaus Havelund, Rupak Majumdar, and Jens Palsberg, editors, Model Checking Software, 15th International SPIN Workshop, Los Angeles, CA, USA, August 10-12, 2008, Proceedings, volume 5156 of Lecture Notes in Computer Science, pages 176–195. Springer, 2008
Stefan Leue, Alin Stefanescu, and Wei Wei
-
An executable and extensible formal semantics for UML-RT. In Holger Giese, Michaela Huhn, Ulrich Nickel, and Bernhard Schätz, editors, Dagstuhl-Workshop MBEES: Modellbasierte Entwicklung eingebetteter Systeme V, Schloss Dagstuhl, Germany, 2009, Tagungsband Modellbasierte Entwicklung eingebetteter Systeme, volume 2009-01 of Informatik-Bericht, pages 182–188. TU Braunschweig, Institut fur Software Systems Engineering, 2009
Stefan Leue and Wei Wei
-
Extending non-termination proof techniques to asynchronously communicating concurrent programs. In Andrei Voronkov, Laura Kovács, and Nikolaj Bjørner, editors, Second International Workshop on Invariant Generation, WING 2009, York, UK, March 29, 2009 and Third International Workshop on Invariant Generation, WING 2010, Edinburgh, UK, July 21, 2010, volume 1 of EPiC Series, pages 132–147. EasyChair, 2010
Matthias Kuntz, Stefan Leue, and Christoph Scheben
-
Counterexample explanation by anomaly detection. In Alastair F. Donaldson and David Parker, editors, Model Checking Software - 19th International Workshop, SPIN 2012, Oxford, UK, July 23-24, 2012. Proceedings, volume 7385 of Lecture Notes in Computer Science, pages 24–42. Springer, 2012
Stefan Leue and Mitra Tabaei Befrouei
-
Integer linear programming-based property checking for asynchronous reactive systems. Software Engineering, IEEE Transactions on, 39(2):216–236, 2013
Stefan Leue and Wei Wei
-
Mining sequential patterns to explain concurrent counterexamples. In Ezio Bartocci and C. R. Ramakrishnan, editors, Model Checking Software - 20th International Symposium, SPIN 2013, Stony Brook, NY, USA, July 8-9, 2013. Proceedings, volume 7976 of Lecture Notes in Computer Science, pages 264–281. Springer, 2013
Stefan Leue and Mitra Tabaei Befrouei
