Ein „Teile-und-Herrsche“-Ansatz zur Lead-to-Modellprüfung für große Systeme

Die Modellprüfung ist eine der erfolgreichsten Errungenschaften der Informatik in den letzten Jahrzehnten. Aus diesem Grund wurden Edmund M. Clarke, E. Allen Emerson und Joseph Sifakis mit dem AM Turing Award 2007 für ihre Rolle bei der Entwicklung der Modellprüfung zu einer hochwirksamen Verifizierungstechnologie geehrt.

Die Modellprüfung ist vor allem in der Hardwareindustrie weit verbreitet, da sie ein System, das die gewünschten Eigenschaften erfüllt, systematisch verifizieren kann. Allerdings gibt es bei der Modellprüfung noch einige Probleme zu lösen, darunter die berüchtigte Staatenexplosion. Es wurden viele Techniken zur Abmilderung der Staatsexplosion entwickelt, beispielsweise die teilweise Reduzierung der Ordnung und die Abstraktion.

Trotz dieser vorhandenen Techniken reichen sie möglicherweise nicht aus, um die Staatsexplosion zu bewältigen. Ein weiteres Ziel besteht darin, die Laufleistung der Modellprüfung zu erhöhen. Ein vielversprechender Ansatz zur Lösung dieses Problems ist die Parallelisierung der Modellprüfung, wodurch Multicore-Architekturen optimal genutzt werden können.

Ein Forschungsteam des Japan Advanced Institute of Science and Technology (JAIST) unter der Leitung von Professor Kazuhiro Ogata hat einen „Teile-und-Herrsche“-Ansatz für die Lead-to-Modellprüfung entwickelt, der als DCA2L2MC bezeichnet wird. Wie der Name schon sagt, ist DCA2L2MC Lead-to-Eigenschaften gewidmet, die informell beschreiben, dass, wann immer etwas wahr wird, irgendwann auch etwas anderes wahr wird.

Chandy und Misra entwarfen eine zeitliche Logik namens UNITY, in der die zeitliche Konnektivität „Zuführungen zu“ eine wichtige Rolle spielt, und sie zeigten, dass viele wesentliche Systemanforderungen als Eigenschaften zu „Zuführungen“ ausgedrückt werden können. Daher ist es von Vorteil, sich auf Leads-to-Eigenschaften zu konzentrieren. Details zu DCA2L2MC wurden in einem Artikel in veröffentlicht ACM-Transaktionen zu Software-Engineering und -Methodik.

Die Kernidee von DCA2L2MC besteht darin, ein ursprüngliches Lead-to-Model-Checking-Problem geschichtet in mehrere kleinere Model-Checking-Probleme aufzuteilen und jedes kleinere Problem unabhängig voneinander anzugehen. Insbesondere unterteilt DCA2L2MC den erreichbaren Zustandsraum von jedem Anfangszustand in L+1 Schichten, wobei L eine positive natürliche Zahl ist, wodurch mehrere Unterzustandsräume erzeugt werden. Modellüberprüfungsexperimente werden dann für jeden Unterzustandsraum statt für den ursprünglich erreichbaren Zustandsraum durchgeführt.

Wenn jeder Unterzustandsraum viel kleiner ist als der ursprünglich erreichbare Zustandsraum, wird es möglich, eine Lead-to-Modellprüfung durchzuführen, selbst wenn eine direkte Durchführung für den ursprünglich erreichbaren Zustandsraum aufgrund des Problems der Zustandsraumexplosion nicht möglich ist. Dies ist der Schlüssel zur Minderung des Problems der Zustandsraumexplosion bei der Modellprüfung mit DCA2L2MC.

Darüber hinaus kann aufgrund der Natur des Divide-and-Conquer-Ansatzes jedes kleinere Modellprüfungsproblem unabhängig gelöst werden. Insbesondere kleinere Modellprüfungsprobleme in der letzten Schicht unserer Abteilung sind völlig unabhängig. Dies ist der Schlüssel zur Verbesserung der Laufleistung der Modellprüfung durch Verwendung der Parallelisierung für DCA2L2MC.

Aus theoretischer Sicht haben die Forscher einen Satz bewiesen, der die Korrektheit von DCA2L2MC garantiert und zeigt, dass die Probleme mit mehreren Modellprüfungen dem ursprünglichen Problem der Leads-to-Model-Prüfung äquivalent sind. Im praktischen Bereich haben sie in Maude ein Support-Tool für DCA2L2MC entwickelt, eine leistungsstarke Spezifikations-/Programmiersprache, die auf Rewriting-Logik basiert. Dieses Support-Tool bietet die Flexibilität, je nach Bedarf im sequentiellen und parallelen Modus ausgeführt zu werden.

Es wurden mehrere Fallstudien durchgeführt, um die Wirksamkeit und Effizienz des Ansatzes bei der Modellprüfung von Leads-to-Eigenschaften zu demonstrieren. Darüber hinaus haben sie gezeigt, dass DCA2L2MC im Vergleich zu bestehenden Modellprüfern wie SPIN und LTSMin als Technik zur Modellprüfung von Lead-to-Eigenschaften in großen Systemen vielversprechend ist.

Um DCA2L2MC optimal zu nutzen, haben die Forscher zwei Optimierungstechniken vorgeschlagen: eine zum gleichzeitigen Finden aller Gegenbeispiele bei der Modellprüfung mithilfe eines neuen Modellprüfers und eine weitere zum Finden einer guten Schichtkonfiguration für DAC2L2MC mithilfe eines Analysetools. Die erste Technik spielt eine entscheidende Rolle bei der effizienten Generierung aller Gegenbeispiele in DCA2L2MC und verbessert die Laufleistung erheblich. Die zweite Technik ist wichtig, um eine gute Layer-Konfiguration zu finden, die die Laufleistung von DCA2L2MC optimiert. Durch die Verwendung dieser beiden Optimierungstechniken wird DCA2L2MC bei der Verifizierung effektiver und effizienter.

Schließlich kann DCA2LCMC in bestehende Modellprüfer integriert werden, wodurch diese in die Lage versetzt werden, Modellprüfungen auf größeren Systemen durchzuführen. Die Forscher hoffen, dass mehrere bestehende Modellprüfer DCA2LCMC als effektive und effiziente Technik zur Handhabung von Leads-to-Eigenschaften nutzen werden. Darüber hinaus können Forscher und Ingenieure die Technik und das Werkzeug problemlos übernehmen, um die Verifizierung von Systemen mit Lead-to-Eigenschaften durchzuführen.

Bereitgestellt vom Japan Advanced Institute of Science and Technology