Model Checking

Model Checking

Model Checking (deutsch auch Modellprüfung) ist ein Verfahren zur vollautomatischen Verifikation einer Systembeschreibung (Modell) gegen eine Spezifikation (Formel). Der Begriff ist motiviert durch die mathematische Formulierung des Problems: Für eine gegebene Systembeschreibung M und eine gegebene logische Eigenschaft ϕ, prüfe, ob M Modell ist für ϕ (formal M \models \phi).

Das Verfahren wird als vollautomatisch bezeichnet, weil es keiner Benutzerinteraktion bedarf (im Gegensatz zu einigen deduktiven Verfahren, wie zum Beispiel interaktives Theorembeweisen). Die Systembeschreibung erfolgt in einer formalen Sprache, zum Beispiel durch ein Programm, einen endlichen Automaten oder ein Transitionssystem. Der Zustandsraum des Systems muss nicht notwendigerweise endlich, jedoch endlich repräsentierbar sein. Die Spezifikation ist die nachzuweisende formale Eigenschaft des Systems, gegeben zum Beispiel durch eine temporal-logische Formel oder durch einen Beobachtungsautomaten.

Inhaltsverzeichnis

Prinzip

Eingabe des Modellprüfers (engl. model checkers) sind die Systembeschreibung und die Spezifikation. Erfüllt die Systembeschreibung die Spezifikation, stoppt der Algorithmus und liefert ein Korrektheitszertifikat als Ausgabe. Findet der Algorithmus eine Verletzung der Spezifikation, stoppt der Algorithmus und liefert als Ausgabe ein Gegenbeispiel. Dies ist meist eine mögliche Systemausführung, die das Verletzen der Spezifikation nachweist.

Temporal-logische Logiken

Bei der logischen Formel, der formalisierten Spezifikation, handelt es sich oft um eine Formel einer temporalen Logik. Diese macht eine Aussage über das zu prüfende Verhalten des Systems über die Zeit (z.B. In keiner Ausführung kommt es zu einem Deadlock). Solche Eigenschaften lassen sich in einer der folgenden häufig verwendeten Logiken ausdrücken.

Beim modalen μ-Kalkül handelt es sich um ein auf Fixpunktoperatoren über den Zuständen des Modelles beruhenden Ansatz (in der Liste der genannten Logiken stellt er die mächtigste Logik dar und umfasst die anderen). In der praktischen Anwendung sind die Logiken CTL*, CTL und LTL jedoch weitaus häufiger vertreten.

CTL* stellt eine Obermenge der beiden Logiken CTL und LTL dar. Ferner lassen sich Aussagen aus CTL und LTL i.A. nicht ineinander überführen.

Typen von Algorithmen des Model Checkings

Die Algorithmen des Model Checkings werden in zwei Typen unterschieden.

Explizites Model Checking

Explizites Model Checking baut das Transitionssystem in geeigneter Weise auf und exploriert es bzgl. der zu prüfenden Eigenschaft.

Automaten-basiertes LTL-Model Checking

Ein bekannter Ansatz zum Verifizieren von LTL-Formeln benutzt Büchi-Automaten. Hierbei werden zunächst sowohl das zu prüfende System als auch die Eigenschaft selbst in einen Büchi-Automaten überführt. Diese Automaten seien mit B(M) bzw. B(ϕ) bezeichnet.

Nun erfüllt das System M die Eigenschaft ϕ genau dann, wenn B(M) eine Teilmenge der zulässigen durch den Eigenschaftsautomaten B(ϕ) beschriebenen Systemevolutionen realisieren kann; wenn also für die durch die Büchi-Automaten beschriebenen Sprachen folgende Inklusionsbeziehung gilt:

Lang(B(M)) \subseteq Lang(B(\phi)).

Dies lässt sich umformen zu

Lang(B(M)) \cap \overline{Lang(B(\phi))} = \emptyset.

Dies ist wiederum äquivalent zu

Lang(B(M)) \cap Lang(B(\neg\phi)) = \emptyset bzw. Lang(B(M) \cap B(\neg\phi)) = \emptyset.

Es reicht also, für die negierte Eigenschaft einen Büchi-Automaten zu konstruieren und diesen mit dem für das System konstruierten Büchi-Automaten zu verschneiden. Beschreibt das Ergebnis die leere Sprache, so ist die Eigenschaft erfüllt. Ansonsten beschreibt der resultierende Automat genau die Systemevolutionen, die zum Scheitern der Eigenschaft führten.

CTL-Model Checking

Bei CTL-Formeln werden an den Zuständen schrittweise Teilformeln auf ihre Wahrheitswerte überprüft.

Der Zustandsraumexplosion kann z.B. durch Ausnutzen von Symmetrien und Partial Order Reduction entgegengewirkt werden, um möglichst große Transitionssysteme verifizieren zu können.

Symbolisches Model Checking

Symbolische Modellprüfer basieren entweder auf Binären Entscheidungsdiagrammen (z. B. für CTL-Formeln) oder auf SAT-Solvern (z.B. für LTL-Formeln). Im ersten Fall wird je ein BDD (engl. binary decision diagram, Binäres Entscheidungsdiagramm) für die Zustandsübergangsrelation und die erfüllbaren Zustände der Formel aufgebaut. Im zweiten Fall werden Modell und Spezifikation in eine aussagenlogische Formel umgewandelt, die anschließend auf Erfüllbarkeit überprüft wird.

Praktischer Einsatz

Seit Anfang der 90er Jahre wurden große Fortschritte in der Performance der Algorithmen erzielt, wodurch das Verfahren für die Praxis interessant geworden ist. In der Qualitätssicherung beim Entwurf großer integrierter Schaltungen werden Modellprüfer bereits in der industriellen Praxis eingesetzt. In den letzten Jahren wurden in einigen Forschungsprojekten Modellprüfer für Software entwickelt.

Literatur

Grundlegende Einfuehrung mit sehr vielen Beispielen.
(Gilt als erste größere zusammenfassende Veröffentlichung, bisher Standardwerk auf dem Gebiet.)
  • Peled: Software Reliability Methods. Springer-Verlag, 2001. ISBN 0-387-95106-7
  • B. Berard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit, L. Petrucci, P. Schnoebelen: Systems and Software Verification: Model-Checking Techniques and Tools, ISBN 3-540-41523-8
(Neben einem Teil mit theoretischen Grundlagen und anschaulichen Beispielen, stellt das Buch in einem zweiten Teil diverse unterschiedliche Werkzeuge und deren typische Anwendungsgebiete vor.)
(In einer kurzen Übersicht werden unterschiedliche Modellierungtypen sowie Logiken und im speziellen der modale Mu-Kalkül vorgestellt.)

Wikimedia Foundation.

Игры ⚽ Поможем решить контрольную работу

Schlagen Sie auch in anderen Wörterbüchern nach:

  • Model Checking — Le Model Checking désigne une famille de techniques de vérification automatique des systèmes dynamiques (souvent d origine informatique ou électronique). Il s agit de vérifier algorithmiquement si un modèle donné, le système lui même ou une… …   Wikipédia en Français

  • Model checking — This article is about checking of models in computer science. For the checking of models in statistics, see regression model validation. In computer science, model checking refers to the following problem: Given a model of a system, test… …   Wikipedia

  • Model checking — Le Model Checking désigne une famille de techniques de vérification automatique des systèmes dynamiques (souvent d origine informatique ou électronique). Il s agit de vérifier algorithmiquement si un modèle donné, le système lui même ou une… …   Wikipédia en Français

  • Model checking — Con el nombre Model checking se conoce a un método automático de verificación de un sistema formal, en la mayoría de las ocasiones derivado del hardware o del software de un sistema informático. El sistema es descrito mediante un modelo, que debe …   Wikipedia Español

  • Model checking (disambiguation) — Model checking may refer to model checking regression model validation This disambiguation page lists articles associated with the same title. If an internal link led you here, you may wish to chan …   Wikipedia

  • Abstraction model checking — is for systems where an actual representation is too complex in developing the model alone. So, the design undergoes a kind of translation to scaled down abstract version.The set of variables are partitioned into visible and invisible depending… …   Wikipedia

  • Model-based testing — is the application of Model based design for designing and optionally executing the necessary artifacts to perform software testing. Models can be used to represent the desired behavior of the System Under Test (SUT), or to represent the desired… …   Wikipedia

  • Model audit — A model audit is the colloquial term for the tasks performed when conducting due diligence on a financial model, in order to eliminate spreadsheet error. (Also known as Model Review in some areas). A study in 1998 concluded that even MBA students …   Wikipedia

  • Model theory — This article is about the mathematical discipline. For the informal notion in other parts of mathematics and science, see Mathematical model. In mathematics, model theory is the study of (classes of) mathematical structures (e.g. groups, fields,… …   Wikipedia

  • Model View ViewModel — The Model View ViewModel (MVVM) is an architectural pattern used in software engineering that originated from Microsoft as a specialization of the Presentation Model design pattern introduced by Martin Fowler.[1] Largely based on the Model view… …   Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”