www.wikidata.de-de.nina.az

Model Checking deutsch auch Modellprüfung ist ein Verfahren zur vollautomatischen Verifikation einer Systembeschreibung

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 und eine gegebene logische Eigenschaft , prüfe, ob Modell ist für (formal ).

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.

Prinzip Bearbeiten

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 Bearbeiten

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 Bearbeiten

Die Algorithmen des Model Checkings werden in zwei Typen unterschieden.

Explizites Model Checking Bearbeiten

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

Automaten-basiertes LTL-Model Checking Bearbeiten

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 bzw. bezeichnet.

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

.

.

bzw. .

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 Bearbeiten

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 Bearbeiten

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 Bearbeiten

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.

Erweiterungen Bearbeiten

Klassisches Model Checking bezieht quantitative Aspekte wie Wahrscheinlichkeiten oder Kosten nicht in die Analyse mit ein. Daher werden im quantitativen Model Checking Fragestellungen betrachtet wie:

  • Mit welcher Wahrscheinlichkeit gilt eine Eigenschaft?
  • Liegt die Wahrscheinlichkeit dafür, dass die Eigenschaft erfüllt ist, über/unter einer gegebenen Schranke?
  • Liegen die Kosten, die notwendig sind, um Eigenschaft zu erfüllen, innerhalb eines gegebenen Kostenrahmens?

Solche Eigenschaften lassen sich in der Logik PCTL*, einer Erweiterung von CTL*, die die Quantifizierung von Wahrscheinlichkeiten erlaubt, ausdrücken.

Implementierungen Bearbeiten

Literatur Bearbeiten

  • Baier, Katoen: "Principles of Model Checking", MIT Press, 2008. ISBN 978-0-262-02649-9
  • Clarke, Grumberg, Peled: Model Checking. MIT Press, 2000. ISBN 0-262-03270-8
  • 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
wikipedia, wiki, deutsches, deutschland, buch, bücher, bibliothek artikel lesen, herunterladen kostenlos kostenloser herunterladen, MP3, Video, MP4, 3GP, JPG, JPEG, GIF, PNG, Bild, Musik, Lied, Film, Buch, Spiel, Spiele
Veröffentlichungsdatum:
Model Checking deutsch auch Modellprufung ist ein Verfahren zur vollautomatischen Verifikation einer Systembeschreibung Modell gegen eine Spezifikation Formel Der Begriff ist motiviert durch die mathematische Formulierung des Problems Fur eine gegebene Systembeschreibung M displaystyle M und eine gegebene logische Eigenschaft ϕ displaystyle phi prufe ob M displaystyle M Modell ist fur ϕ displaystyle phi formal M ϕ displaystyle 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 reprasentierbar sein Die Spezifikation ist die nachzuweisende formale Eigenschaft des Systems gegeben zum Beispiel durch eine temporal logische Formel oder durch einen Beobachtungsautomaten Inhaltsverzeichnis 1 Prinzip 2 Temporal logische Logiken 3 Typen von Algorithmen des Model Checkings 3 1 Explizites Model Checking 3 1 1 Automaten basiertes LTL Model Checking 3 1 2 CTL Model Checking 3 2 Symbolisches Model Checking 4 Praktischer Einsatz 5 Erweiterungen 6 Implementierungen 7 LiteraturPrinzip BearbeitenEingabe des Modellprufers engl model checkers sind die Systembeschreibung und die Spezifikation Erfullt 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 mogliche Systemausfuhrung die das Verletzen der Spezifikation nachweist Temporal logische Logiken BearbeitenBei der logischen Formel der formalisierten Spezifikation handelt es sich oft um eine Formel einer temporalen Logik Diese macht eine Aussage uber das zu prufende Verhalten des Systems uber die Zeit z B In keiner Ausfuhrung kommt es zu einem Deadlock Solche Eigenschaften lassen sich in einer der folgenden haufig verwendeten Logiken ausdrucken CTL Lineare temporale Logik kurz LTL Modaler m KalkulBeim modalen m Kalkul handelt es sich um ein auf Fixpunktoperatoren uber den Zustanden des Modelles beruhenden Ansatz in der Liste der genannten Logiken stellt er die machtigste Logik dar und umfasst die anderen In der praktischen Anwendung sind die Logiken CTL CTL und LTL jedoch weitaus haufiger vertreten CTL stellt eine Obermenge der beiden Logiken CTL und LTL dar Ferner lassen sich Aussagen aus CTL und LTL i A nicht ineinander uberfuhren Typen von Algorithmen des Model Checkings BearbeitenDie Algorithmen des Model Checkings werden in zwei Typen unterschieden Explizites Model Checking Bearbeiten Explizites Model Checking baut das Transitionssystem in geeigneter Weise auf und exploriert es bzgl der zu prufenden Eigenschaft Automaten basiertes LTL Model Checking Bearbeiten Ein bekannter Ansatz zum Verifizieren von LTL Formeln benutzt Buchi Automaten Hierbei werden zunachst sowohl das zu prufende System als auch die Eigenschaft selbst in einen Buchi Automaten uberfuhrt Diese Automaten seien mit B M displaystyle B M nbsp bzw B ϕ displaystyle B phi nbsp bezeichnet Nun erfullt das System M displaystyle M nbsp die Eigenschaft ϕ displaystyle phi nbsp genau dann wenn B M displaystyle B M nbsp eine Teilmenge der zulassigen durch den Eigenschaftsautomaten B ϕ displaystyle B phi nbsp beschriebenen Systemevolutionen realisieren kann wenn also fur die durch die Buchi Automaten beschriebenen Sprachen folgende Inklusionsbeziehung gilt L a n g B M L a n g B ϕ displaystyle Lang B M subseteq Lang B phi nbsp Dies lasst sich umformen zuL a n g B M L a n g B ϕ displaystyle Lang B M cap overline Lang B phi emptyset nbsp Dies ist wiederum aquivalent zuL a n g B M L a n g B ϕ displaystyle Lang B M cap Lang B neg phi emptyset nbsp bzw L a n g B M B ϕ displaystyle Lang B M cap B neg phi emptyset nbsp Es reicht also fur die negierte Eigenschaft einen Buchi Automaten zu konstruieren und diesen mit dem fur das System konstruierten Buchi Automaten zu verschneiden Beschreibt das Ergebnis die leere Sprache so ist die Eigenschaft erfullt Ansonsten beschreibt der resultierende Automat genau die Systemevolutionen die zum Scheitern der Eigenschaft fuhrten CTL Model Checking Bearbeiten Bei CTL Formeln werden an den Zustanden schrittweise Teilformeln auf ihre Wahrheitswerte uberpruft Der Zustandsraumexplosion kann z B durch Ausnutzen von Symmetrien und Partial Order Reduction entgegengewirkt werden um moglichst grosse Transitionssysteme verifizieren zu konnen Symbolisches Model Checking Bearbeiten Symbolische Modellprufer basieren entweder auf Binaren Entscheidungsdiagrammen z B fur CTL Formeln oder auf SAT Solvern z B fur LTL Formeln Im ersten Fall wird je ein BDD engl binary decision diagram Binares Entscheidungsdiagramm fur die Zustandsubergangsrelation und die erfullbaren Zustande der Formel aufgebaut Im zweiten Fall werden Modell und Spezifikation in eine aussagenlogische Formel umgewandelt die anschliessend auf Erfullbarkeit uberpruft wird Praktischer Einsatz BearbeitenSeit Anfang der 90er Jahre wurden grosse Fortschritte in der Performance der Algorithmen erzielt wodurch das Verfahren fur die Praxis interessant geworden ist In der Qualitatssicherung beim Entwurf grosser integrierter Schaltungen werden Modellprufer bereits in der industriellen Praxis eingesetzt In den letzten Jahren wurden in einigen Forschungsprojekten Modellprufer fur Software entwickelt Erweiterungen BearbeitenKlassisches Model Checking bezieht quantitative Aspekte wie Wahrscheinlichkeiten oder Kosten nicht in die Analyse mit ein Daher werden im quantitativen Model Checking Fragestellungen betrachtet wie Mit welcher Wahrscheinlichkeit gilt eine Eigenschaft Liegt die Wahrscheinlichkeit dafur dass die Eigenschaft erfullt ist uber unter einer gegebenen Schranke Liegen die Kosten die notwendig sind um Eigenschaft zu erfullen innerhalb eines gegebenen Kostenrahmens Solche Eigenschaften lassen sich in der Logik PCTL einer Erweiterung von CTL die die Quantifizierung von Wahrscheinlichkeiten erlaubt ausdrucken Implementierungen BearbeitenSPIN Marcie Prism Uppaal QuantUMLiteratur BearbeitenBaier Katoen Principles of Model Checking MIT Press 2008 ISBN 978 0 262 02649 9Grundlegende Einfuehrung mit sehr vielen Beispielen Clarke Grumberg Peled Model Checking MIT Press 2000 ISBN 0 262 03270 8 Gilt als erste grossere zusammenfassende Veroffentlichung 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 Julian Bradfield Colin Stirling Modal logics and mu calculi GZIP 144 kB Markus Muller Olm David A Schmidt Bernhard Steffen Model checking a tutorial introduction GZIP 140 kB Proc 6th Static Analysis Symposium G File and A Cortesi eds Springer LNCS 1694 1999 pp 330 354 In einer kurzen Ubersicht werden unterschiedliche Modellierungtypen sowie Logiken und im Speziellen der modale Mu Kalkul vorgestellt Abgerufen von https de wikipedia org w index php title Model Checking amp oldid 232824606