Loading…
Model checking combined Z and Statechart specifications
Büssow, Robert
Eine der bedeutendsten Herausforderungen der Softwareentwicklung besteht darin, einen Entwicklungsprozess zu garantieren, der Fehlerfreiheit nicht nur gewährleistet sondern auch nachweisbar macht. Beides ist von besonderer Bedeutung, wenn sicherheitskritische Systeme entwickelt werden, etwa in den Bereichen der Medizin, der Produktionssteuerung oder der Verkehrstechnik. Softwarefehler können hier lebensbedrohlich sein. Aus diesem Grund ist es meist auch notwendig, die Fehlerfreiheit der Software einem Dritten nachzuweisen. Die Steuerung einer Verkehrsampel muss beispielsweise nicht nur fehlerfrei funktionieren, sondern auch vom TÜV abgenommen werden. Der Einsatz formaler Methoden stellt einen vielversprechenden Ansatz dar, diese Probleme zu lösen. Formale Sprachen haben gegenüber den üblichen, nicht-formalen Methoden (umgangssprachliche Spezifikationsdokumente oder Spezifikationssprachen ohne eindeutige Semantik) den Vorteil einer eindeutigen Semantik. Damit können Anforderungen an ein System eindeutig beschrieben und seine Eigenschaften mathematisch bewiesen werden. In der Praxis haben sich diese Methoden allerdings bisher noch nicht durchgesetzt. Zwei herausragende Ursachen hierfür sind: 1. Die formalen Spezifikationssprachen orientieren sich meist mehr an mathematischer Eleganz als an einfachen und intuitiven Sprachmitteln. Das stellt eine große Hürde für den praktischen Einsatz dar. Die Spezifikationssprache mSZ versucht dieses Problem zu lösen. Sie verbindet die von Harel entwickelte und in der Industrie akzeptierte grafische Sprache Statecharts mit der formalen Sprache Z. Damit liegt eine intuitive Sprache vor, die den Anforderungen einer formalen Sprache genügt. 2.Formale Spezifikationen haben zwar eine präzise Semantik, sie lassen aber dem Spezifikateur immer noch die Freiheit, inkonsistente oder fehlerhafte (nicht den tatsächlichen Anforderungen entsprechende) Spezifikationen zu erstellen. Andererseits ermöglichen sie es, Konsistenz und Eigenschaften formal zu beweisen und so zu einer fehlerfreien Spezifikation zu gelangen. Werden solche Beweise nicht geführt, ist gegenüber einer nicht-formalen Spezifikation wenig gewonnen. Um die aufwändige Beweisführung praktikabel zu machen, ist eine möglichst weitgehende Automatisierung unverzichtbar. Der Nachweis der Konsistenz sowie der Eigenschaften einer mSZ Spezifikation ist Ziel der vorliegenden Arbeit. Hierfür werden Model Checking Techniken eingesetzt. Um dies zu ermöglichen, wird die mSZ Spezifikation in drei Schritten übersetzt: 1. Übersetzung des Statechartanteils einer mSZ-Spezifikation nach Z. Damit werden zusätzlich die Semantik der Statecharts und die Semantik die Integration von Statecharts und Z definiert. Außerdem erlaubt diese Vorgehensweise andere, reine Z-Werkzeuge für die Analyse zu benutzen. 2. Vereinfachung der Z-Spezifikation in ein vereinfachtes Z (Simple Z), das vom Sprachumfang der Eingabesprache eines Model Checkers entspricht. Dieser Schritt erlaubt es, sowohl mSZ-Spezifikationen wie auch reine Z Spezifikationen für das Model Checking vorzubereiten. Das vereinfachte Z kann leicht in die Eingabesprache eines Model Checkers übersetzt werden. 3. Übersetzung von Simple Z in die Eingabesprache des SMV Model Checkers von McMillan. Der Model Checker kann dann Konsistenz und Eigenschaften der Spezifikation beweisen.
One of today's major problems in software engineering is to achieve a high and comprehensive quality standard for the software development process, in order to maintain a reliable high quality for the resulting products. This holds particularly true for safety critical systems, where failure of the software may have life-threatening consequences. Here, not only the quality of the software itself is important, but also the ability to convince a third party of this very quality. The usage of formal methods is one promising approach to achieve these goals. Roughly speaking, formal methods introduce mathematical precision to the development process. They do so by using formalisms with well defined semantics, and so stipulate formal proofs to verify development steps. This approach is all too well feasible in theory. In practice, however, one will encounter various problems that impede a consequent usage of formal methods: 1. The formal character of the proposed languages and the need to use them for every aspect of the described system makes them too bulky. The reason for this is that they often times concentrate more on the mathematical elegance of their underlying semantics than on comfortable and intuitive usage. The specification language mSZ tackles this problem. It combines Harel s Statecharts with the formal specification language Z and offers very intuitive means to describe a system. 2. As adequate tool support is often missing, implementation of the formal proof obligations becomes practically impossible, because without any tools, these proofs are quite complicated, and their development takes a lot of time. Providing tool support for the verification of consistency and properties of an mSZ specification is the objective of this work. Model checking is used for the verification. An mSZ specification is translated in three steps into the input language of a model checker: 1. The Statecharts are translated to Z. With this, the Statechart semantics and the semantics of the Statechart integration with Z are defined. The result of this translation can also be used by Z tools that do not know Statecharts for analysis. 2. The Z specification is rewritten to a Z subset (Simple Z) that contains only language constructs, supported by the model checker. This step allows preparing mSZ as well as pure Z specifications for model checking. 3. Simple Z is translated to the input language of the SMV model checker.
