Diskussion:Model Checking

Quellen fuer Bewertung der Model-Checking-Tools

Woher stammen die Bewertungen unter der der Ueberschrift 5 (Maßstab: { sehr schlecht } --- | -- | - | o | + | ++ | +++ { sehr gut } oder { niedrig } bis { hoch })?

Moege der/die AutorIn dieses Abschnittes die Quellen angeben..

Symbolisches Model Checking

Der Abschnitt zum symbolischen Model Checking ist so falsch. Beispielsweise die weiterführenden Arbeiten von E. Clarke wiederlegen die Behauptungen dort. Dort werden u.A. SAT Solver für ECTL* und ACTL* benutzt. Außerdem kann man mit BDDs µ-Calculus benutzen (was deutlich stärker als CTL ist).

Momentan fehlt mir die Zeit den Artikel zu verbessern, werde mich aber hoffentlich bald daran machen können.

Das Tool [mc]square benutzt übrigens auch symbolisches Model-Checking um CTL Formeln zu überprüfen!

Abgesehen davon, dass ich mich mit den aktuellen Entwicklungen nicht auskenne. Wo behauptet der Artikel das Gegenteil? E. Clarke (wer auch immer das ist) wiederlegt ganz sicher nicht, dass man das dort beschriebene tun kann, schließlich wird/wurde es getan!? Niemand hat behauptet, das nicht mehr möglich ist. Also bitte mal die Behauptungen präzisieren/richtigstellen! --Koethnig 14:00, 16. Jan. 2007 (CET)

Jetzt nicht mehr. Als ich den Kommentar geschrieben habe, hatte der Artikel noch 3 "z.B." weniger. Da standen in den Klammern keine "z.B.", so dass der Eindruck entstand, dass dies verbindlich wäre. Dem widerspricht Clarke dadurch, dass er auch CTL-Formeln mit SAT-Methoden bearbeitet. Edmund Clarke ist Professor an der Carnegie Mellon University und Autor der einzigen Quelle des Artikels, daher habe ich mich auf ihn bezogen. In der aktuellen Version ist der Artikel zwar noch sehr oberflächlich, aber zumindest nicht mehr falsch, da die kritischen Behauptungen durch "z.B." entschärft wurden.

Jo, die "z.B." habe ich eingefügt, weil ohne wars tatsächlich irreführend, aber die Worte "falsch" oder "wiederlegt" fand ich doch etwas übertrieben. Die Quelle kenn ich nicht, die hat jemand anderes hinzugefügt! Möglicherweise war es auch eine Quelle meines damaligen Dozenten?! --Koethnig 00:28, 17. Jan. 2007 (CET)

Explizites Model Checking

Reduktionen durch partielle Ordnungen und Bisimulation sind nicht fester Bestandteil des expliziten Model Checkings und nur ein winziger Teil Werkzeuge mit denen man den Zustandsraum kleiner kriegt. Solche Verbesserungen sollten einen eigenen Abschnitt bekommen und um wichtigere Techniken wie On-The-Fly und Abstraktion erweitert werden. Außerdem könnte man die Model Checking Algorithmen (in Pseudo Code) angeben.

Wo bitte im Artkiel kommt das Wort Bisimulation vor? Wo steht, dass es zusammen mit partial order reduktion "fester Bestandteil" sei? Natürlich sind weitere Verfahren möglich und denkbar! --Koethnig 14:00, 16. Jan. 2007 (CET)

"Ausnutzen von Symmetrien" in Verbindung mit "Partial Order Reduction" brachte mich dazu davon auszugehen, dass der Autor von Bisimulation spricht (also der Reduktion des Zustandsraums durch einen Bisimulations-Quotienten). Auch hier fehlte das "z.B." und das "kann", so dass der Eindruck entstand, diese Techniken seien Teil des Model Checking Algorithmus.

"Bisimulation" habe ich noch nie gehört. Aber ich hatte ja auch nur eine Vorlesung zu dem Thema und die ist wie gesagt schon ne Weile her. Symmetrien und Partial Order Reduktion sind so weit ich mich erinnere unabhängige aber gleichzeitig funktioierende Konzepte zur Reduktion des Zustandsraumes. Aber nach 2 Jahren leg ich meine Hand dafür auch nichts mehr ins Feuer und das Skript kram ich jetzt auch nicht mehr raus :-). --Koethnig 00:28, 17. Jan. 2007 (CET)

Modellprüfung zurück nach Model Checking verschieben?

Was haltet ihr davon, den Artikel zurück nach Model Checking zu verschieben und eine Weiterleitung von Modellprüfung dorthin anzulegen? Ich finde die deutsche Übersetzung sehr künstlich. Auch viele Vorlesungen an deutschen Unis benutzen dieses Wort nicht, sondern den englischen Term.

Eine kurze Anfrage bei Google liefert 27.900 Seiten aus dem deutschsprachigen Raum für Model Checking, jedoch nur 4.820 für Modellprüfung. --Marco Bakera 08:57, 2. Mai 2008 (CEST)

wurde erledigt. --84.188.197.181 13:11, 9. Nov. 2008 (CET)

Danke. :) --Marco Bakera 22:22, 30. Nov. 2008 (CET)

Endlicher Zustandsraum

Im zweiten Absatz steht: "Der Zustandsraum des Systems muss nicht notwendigerweise endlich, jedoch endlich repräsentierbar sein." Das glaube ich so irgendwie nicht. Wenn der Zustandsraum unendlich sein darf, dann kann man mit Model Checking plötzlich das Halteproblem entscheiden, oder nicht?

Und überhaupt, was heißt "endlich repräsentierbar"? Die Menge der reellen Zahlen ist auch endlich repräsentierbar, nämlich durch den einzelnen Buchstaben $\mathbb {R}$. Und die Menge der reellen Zahlen ist wirklich eine sehr große Menge (überabzählbar). --OmicronPersei8 22:18, 23. Sep. 2008 (CEST)

Nein, warum sollte das so sein? Natürlich können Eigenschaften auf unendlichen Zustandsräumen überprüft werden, ohne dadurch das Halteproblem zu entscheiden. Empfehle dazu, z.B. die Arbeiten von Esparza zu studieren.

Abschnitt Weblinks

bitte mal gemäß Wikipedia:Weblinks entrümpeln. --84.188.197.181 13:11, 9. Nov. 2008 (CET)

Linkfarm entfernt

Folgende Linkfarm habe ich entfernt, vgl. WP:WEB bitte vor erneuter Aufnahme einzelner Links diese einzeln diskutieren: --Complex 09:26, 2. Jan. 2009 (CET)

• EmbeddedValidator, Die Simulink/Stateflow Formale Verifikationsumgebung
• Statemate ModelChecker, Statemate Models Robustness Checking
• Statemate ModelCertifier, Statemate Models Requirements Certification
• Software Modeling and Verification an der RWTH Aachen
• Model Checking an der Carnegie Mellon Universität
• Software Verification and Validation an der UT Austin
• SAnToS Laboratory at K-State
• Automated Software Engineering im Nasa Ames Research Center
• NASA/JPL Laboratory for Reliable Software
• VLSI/CAD Forschungsgruppe — Universität Colorado
• Formal Methods Forschungsgruppe, Universität Utah
• Verification and Validation — Brigham Young Universität, Provo, Utah
• ParaDiSe Laboratory — Masaryk Universität in Brno
• VASY Forschungsteam — INRIA Rhône-Alpes, France
• YAHODA — Übersicht diverser Verifikationstools
• Edmund M. Clarke, E. Allen Emerson, Joseph Sifakis: Turing-Preisträger 2007