Incomplete Property Checking for Asynchronous Reactive Systems
Incomplete Property Checking for Asynchronous Reactive Systems
Loading...
Date
2008
Authors
Editors
Journal ISSN
Electronic ISSN
ISBN
Bibliographical data
Publisher
Series
URI (citable link)
International patent number
Link to the license
EU project number
Project
Open Access publication
Collections
Title in another language
Unvollständige Eigenschaftsüberprüfung für Asynchrone Reaktive Systeme
Publication type
Dissertation
Publication status
Published in
Abstract
Asynchrone Reaktive Systeme kommen in einem breiten Spektrum von Softwaresystemen, so z. B. in Kommunikationsprotokollen und eingebetteten Softwaresystemen, zur Anwendung. Es ist von großer Wichtigkeit zu zeigen, dass diese Systeme korrekt entworfen sind, da ein solcher korrekter Entwurf die Grundlage dafür ist, dass diese Systeme Dienste von hoher Qualität liefern. Formale Ansätze zur Verifikation solcher Systeme, wie z. B. Model Checking, sind aufgrund der extrem großen oder sogar unendlichen Zustandsräume, die diese Systeme besitzen, nur schwer anwendbar. Im Fall von Systemen mit unendlichen Zustandsraum werden viele interessante Verfikationsprobleme unentscheidbar, und traditionelle Model Checking Techniken für endliche Zustandsräume sind dann nicht mehr anwendbar.
Wir schlagen ein auf ganzzahliger Programmierung beruhendes Gerüst zur Verifikation vor, welches auf der lokalen Analyse des zyklischen Verhaltens einer jeden Systemkomponente beruht. Dadurch vermeiden wir die Exploration des sehr großen oder sogar unendlichen Zustandsraums des Systems. Um genau zu sein, verwenden wir automatisierte Abstraktionstechniken, um ein zu analysierendes System in eine Menge von Kontrollflusszyklen zu überführen und den Nachrichten-Austauscheffekt dieser Zyklen zu überapproximieren. Für eine zu analysierende Eigenschaft bestimmen wir notwendige Bedingungen an die Kontrollflusszyklen, welche die Verletzung dieser Eigenschaft anzeigen. Diese Bedingungen werden dann in ein ganzzahliges Programmierungsproblem überführt, so dass dessen Lösungsraum das Eigenschaften verletzende Verhalten des Systems repräsentiert. Die Unlösbarkeit des ganzzahligen Programmierungsproblems beweist damit die Erfüllung der Eigenschaft durch das System. Das ganzzahlige Programmierungsproblem kann dann in polynomieller Zeit auf seine Lösbarkeit hin überprüft werden. Wir haben unser Verifikationsgerüst für die Verifikation der konkreten Eigenschaften der Beschränktheit von Kommunikationspuffern (boundedness of buffers) und der Abwesenheit von divergierendem Systemverhalten (absence of livelock) konkretisiert. Diese beiden Eigenschaften sind für asynchrone reaktive Systeme mit einem unendlichen Zustandsraum unentscheidbar.
Dem gegenüber ist unser Verifikationsgerüst effizient, da es nicht alle exponentiell vielen linearisierten Ausführungsfolgen der Systemkomponenten betrachten muss. Es erhält die Lokalität der Analyse jeder einzelnen Systemkomponente und reduziert das ursprüngliche Verifikationsproblem zu einem Problem, das in polynomieller Zeit gelöst werden kann. Auf der anderen Seite ist unser Verifikationsgerüst unvollständig: es zeigt entweder die Erfüllung einer Eigenschaft, oder es endet mit einem untentschiedenen Verdikt, das wir mit UNKNOWN bezeichnen. In diesem Fall ist die Eigenschaft für das untersuchte System entweder erfüllt, oder nicht erfüllt. Diese Unschärfe wird durch die Grobheit der von unserem Verifikationsgerüst verwendeten Abstraktion hervorgerufen. Die Unvollständigkeit unseres Verfikationsgerüstes ist in jedem Fall unvermeidbar, da die überprüften Eigenschaften unentscheidbar sind.
Da die Präzision unseres auf Abstraktion beruhenden Verifikationsgerüsts ein kritischer Punkt ist, schlagen wir automatische, auf Gegenbeispielen beruhende Abstraktionsverfeinerungsschritte vor. Diese beruhen auf der Entdeckung von Abhängigkeiten zwischen den Kontrollflusszyklen. Die entdeckten Abhängigkeiten können effizient in lineare Ungleichungen übersetzt werden, die dann dazu verwendet werden, die Menge der zur Lösung des ursprünglichen ILP Problems ermittelten linearen Ungleichungen zu erweitern. Die zusätzlichen Ungleichungen schließen möglicherweise nicht zulässiges Verhalten aus, welches zu einer Eigenschaftsverletzung führte, und verfeinern somit die ursprüngliche Abstraktion. Die Methoden zur Entdeckung von Zyklenabhängigkeiten sind ebenfalls unvollständig. Dies bedeutet, dass ein Teil des unzulässigen Verhaltens, das Eigenschaftsverletzungen zur Folge hat, möglicherweise durch die von uns entdeckten Zyklenabhängigkeiten nie entdeckt werden kann.
Die resultierenden Verifikationsverfahren werden durch die Entwicklung von geeigneten Code-Abstraktionstechniken für zwei häufig verwendete Modellierungssprachen, nämlich Promela und UML RT, angepasst. Diese Techniken berücksichtigen spezifische Aspekte der beiden Sprachen, so besonders die Definition von Nachrichten, Prozessinstanziierungen, die Zuweisung von Nachrichtenpuffern, etc. Darüber hinaus haben wir eine automatische, unvollständige Methode zum Beweis der Termination von Programmschleifen entwickelt, welche ohne die explizite Konstruktion von Rangfolge-Funktionen auskommt. Schließlich haben wir mehrere Prototypen-Werkzeuge entwickelt, mit deren Hilfe wir viel versprechende experimentelle Resultate für reale Software-Modelle erhalten haben.
Wir schlagen ein auf ganzzahliger Programmierung beruhendes Gerüst zur Verifikation vor, welches auf der lokalen Analyse des zyklischen Verhaltens einer jeden Systemkomponente beruht. Dadurch vermeiden wir die Exploration des sehr großen oder sogar unendlichen Zustandsraums des Systems. Um genau zu sein, verwenden wir automatisierte Abstraktionstechniken, um ein zu analysierendes System in eine Menge von Kontrollflusszyklen zu überführen und den Nachrichten-Austauscheffekt dieser Zyklen zu überapproximieren. Für eine zu analysierende Eigenschaft bestimmen wir notwendige Bedingungen an die Kontrollflusszyklen, welche die Verletzung dieser Eigenschaft anzeigen. Diese Bedingungen werden dann in ein ganzzahliges Programmierungsproblem überführt, so dass dessen Lösungsraum das Eigenschaften verletzende Verhalten des Systems repräsentiert. Die Unlösbarkeit des ganzzahligen Programmierungsproblems beweist damit die Erfüllung der Eigenschaft durch das System. Das ganzzahlige Programmierungsproblem kann dann in polynomieller Zeit auf seine Lösbarkeit hin überprüft werden. Wir haben unser Verifikationsgerüst für die Verifikation der konkreten Eigenschaften der Beschränktheit von Kommunikationspuffern (boundedness of buffers) und der Abwesenheit von divergierendem Systemverhalten (absence of livelock) konkretisiert. Diese beiden Eigenschaften sind für asynchrone reaktive Systeme mit einem unendlichen Zustandsraum unentscheidbar.
Dem gegenüber ist unser Verifikationsgerüst effizient, da es nicht alle exponentiell vielen linearisierten Ausführungsfolgen der Systemkomponenten betrachten muss. Es erhält die Lokalität der Analyse jeder einzelnen Systemkomponente und reduziert das ursprüngliche Verifikationsproblem zu einem Problem, das in polynomieller Zeit gelöst werden kann. Auf der anderen Seite ist unser Verifikationsgerüst unvollständig: es zeigt entweder die Erfüllung einer Eigenschaft, oder es endet mit einem untentschiedenen Verdikt, das wir mit UNKNOWN bezeichnen. In diesem Fall ist die Eigenschaft für das untersuchte System entweder erfüllt, oder nicht erfüllt. Diese Unschärfe wird durch die Grobheit der von unserem Verifikationsgerüst verwendeten Abstraktion hervorgerufen. Die Unvollständigkeit unseres Verfikationsgerüstes ist in jedem Fall unvermeidbar, da die überprüften Eigenschaften unentscheidbar sind.
Da die Präzision unseres auf Abstraktion beruhenden Verifikationsgerüsts ein kritischer Punkt ist, schlagen wir automatische, auf Gegenbeispielen beruhende Abstraktionsverfeinerungsschritte vor. Diese beruhen auf der Entdeckung von Abhängigkeiten zwischen den Kontrollflusszyklen. Die entdeckten Abhängigkeiten können effizient in lineare Ungleichungen übersetzt werden, die dann dazu verwendet werden, die Menge der zur Lösung des ursprünglichen ILP Problems ermittelten linearen Ungleichungen zu erweitern. Die zusätzlichen Ungleichungen schließen möglicherweise nicht zulässiges Verhalten aus, welches zu einer Eigenschaftsverletzung führte, und verfeinern somit die ursprüngliche Abstraktion. Die Methoden zur Entdeckung von Zyklenabhängigkeiten sind ebenfalls unvollständig. Dies bedeutet, dass ein Teil des unzulässigen Verhaltens, das Eigenschaftsverletzungen zur Folge hat, möglicherweise durch die von uns entdeckten Zyklenabhängigkeiten nie entdeckt werden kann.
Die resultierenden Verifikationsverfahren werden durch die Entwicklung von geeigneten Code-Abstraktionstechniken für zwei häufig verwendete Modellierungssprachen, nämlich Promela und UML RT, angepasst. Diese Techniken berücksichtigen spezifische Aspekte der beiden Sprachen, so besonders die Definition von Nachrichten, Prozessinstanziierungen, die Zuweisung von Nachrichtenpuffern, etc. Darüber hinaus haben wir eine automatische, unvollständige Methode zum Beweis der Termination von Programmschleifen entwickelt, welche ohne die explizite Konstruktion von Rangfolge-Funktionen auskommt. Schließlich haben wir mehrere Prototypen-Werkzeuge entwickelt, mit deren Hilfe wir viel versprechende experimentelle Resultate für reale Software-Modelle erhalten haben.
Summary in another language
Asynchronous reactive systems find applications in a wide range of software systems such as communication protocols, embedded software systems, etc. It is highly desirable to rigorously show that these systems are correctly designed, because a correct design is vital to providing services of high quality. However, formal approaches to the verification of these systems, such as model checking, are often difficult because these systems usually possess extremely large or even infinite state spaces. In fact, in case of infinite state systems, many interesting verification problems become undecidable and traditional finite state model checking techniques cannot be applied to those systems.
We propose an Integer Linear Program (ILP) solving based verification framework that concentrates on the local analysis of the cyclic behavior of each individual component of a system. This way we avoid the exploration of the huge or even infinite state space of the system. More precisely, we use automated abstraction techniques to transform an original system into a set of local control flow cycles and over-approximate the message passing effects of these cycles. Then, we derive a necessary condition for the violation of the considered property on the message passing effects of cycles. We further encode the necessary condition into an ILP problem whose solution space represents the property violating behavior. The infeasibility of the ILP problem then establishes the satisfaction of the property by the system. Moreover, the resulting ILP problem can be checked in polynomial time. We have applied our framework to the verification of the buffer boundedness and livelock freedom properties, both of which are undecidable for asynchronous reactive systems with an infinite state space.
On one hand, the verification framework that we propose is efficient since it needs not to consider an exponential number of all possible interleavings of the executions of the system components. Instead, it maintains the locality of the analysis of each component and reduces the original verification problem into a polynomial-time solvable problem. On the other hand, our framework is incomplete: it either proves the satisfaction of a property, or returns an inconclusive verdict UNKNOWN . In the latter case, the property may or may not be satisfied by the system under scrutiny. This imprecision comes from the potential coarseness of the abstractions that our verification framework employs. After all, the incompleteness of the framework is inevitable since the properties that we check are undecidable.
While the precision of our framework remains an issue, we propose a counterexample guided abstraction refinement procedure based on the discovery of dependencies among control flow cycles. The discovered cycle dependencies can be efficiently encoded into linear inequalities that are used to augment the constraint set of the original property determination ILP problem. The newly added constraints may rule out certain spurious behavior that violates the property, and thus refine the abstraction. The cycle dependency discovery methods that we devise are also incomplete. This means that some spurious property violating behavior may never be eliminated by any cycle dependencies that we can discover.
We make the verification methods applicable to two widely used modeling languages, namely Promela and UML RT, by devising tailored code abstraction techniques. These techniques address abstraction issues concerning specific features of the two languages, such as message definitions, process instantiations, buffer assignments, etc. In particular, we have developed an incomplete automated termination proving technique for program loops, which does not rely on the explicit construction of ranking functions. Finally, we implemented several prototype tools with which we obtained promising experimental results on real life system models.
We propose an Integer Linear Program (ILP) solving based verification framework that concentrates on the local analysis of the cyclic behavior of each individual component of a system. This way we avoid the exploration of the huge or even infinite state space of the system. More precisely, we use automated abstraction techniques to transform an original system into a set of local control flow cycles and over-approximate the message passing effects of these cycles. Then, we derive a necessary condition for the violation of the considered property on the message passing effects of cycles. We further encode the necessary condition into an ILP problem whose solution space represents the property violating behavior. The infeasibility of the ILP problem then establishes the satisfaction of the property by the system. Moreover, the resulting ILP problem can be checked in polynomial time. We have applied our framework to the verification of the buffer boundedness and livelock freedom properties, both of which are undecidable for asynchronous reactive systems with an infinite state space.
On one hand, the verification framework that we propose is efficient since it needs not to consider an exponential number of all possible interleavings of the executions of the system components. Instead, it maintains the locality of the analysis of each component and reduces the original verification problem into a polynomial-time solvable problem. On the other hand, our framework is incomplete: it either proves the satisfaction of a property, or returns an inconclusive verdict UNKNOWN . In the latter case, the property may or may not be satisfied by the system under scrutiny. This imprecision comes from the potential coarseness of the abstractions that our verification framework employs. After all, the incompleteness of the framework is inevitable since the properties that we check are undecidable.
While the precision of our framework remains an issue, we propose a counterexample guided abstraction refinement procedure based on the discovery of dependencies among control flow cycles. The discovered cycle dependencies can be efficiently encoded into linear inequalities that are used to augment the constraint set of the original property determination ILP problem. The newly added constraints may rule out certain spurious behavior that violates the property, and thus refine the abstraction. The cycle dependency discovery methods that we devise are also incomplete. This means that some spurious property violating behavior may never be eliminated by any cycle dependencies that we can discover.
We make the verification methods applicable to two widely used modeling languages, namely Promela and UML RT, by devising tailored code abstraction techniques. These techniques address abstraction issues concerning specific features of the two languages, such as message definitions, process instantiations, buffer assignments, etc. In particular, we have developed an incomplete automated termination proving technique for program loops, which does not rely on the explicit construction of ranking functions. Finally, we implemented several prototype tools with which we obtained promising experimental results on real life system models.
Subject (DDC)
004 Computer Science
Keywords
Program Termination,Control Flow Cycles
Conference
Review
undefined / . - undefined, undefined. - (undefined; undefined)
Cite This
ISO 690
WEI, Wei, 2008. Incomplete Property Checking for Asynchronous Reactive Systems [Dissertation]. Konstanz: University of KonstanzBibTex
@phdthesis{Wei2008Incom-5547,
year={2008},
title={Incomplete Property Checking for Asynchronous Reactive Systems},
author={Wei, Wei},
address={Konstanz},
school={Universität Konstanz}
}
RDF
<rdf:RDF
xmlns:dcterms="http://purl.org/dc/terms/"
xmlns:dc="http://purl.org/dc/elements/1.1/"
xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
xmlns:bibo="http://purl.org/ontology/bibo/"
xmlns:dspace="http://digital-repositories.org/ontologies/dspace/0.1.0#"
xmlns:foaf="http://xmlns.com/foaf/0.1/"
xmlns:void="http://rdfs.org/ns/void#"
xmlns:xsd="http://www.w3.org/2001/XMLSchema#" >
<rdf:Description rdf:about="https://kops.uni-konstanz.de/server/rdf/resource/123456789/5547">
<dcterms:abstract xml:lang="deu">Asynchrone Reaktive Systeme kommen in einem breiten Spektrum von Softwaresystemen, so z. B. in Kommunikationsprotokollen und eingebetteten Softwaresystemen, zur Anwendung. Es ist von großer Wichtigkeit zu zeigen, dass diese Systeme korrekt entworfen sind, da ein solcher korrekter Entwurf die Grundlage dafür ist, dass diese Systeme Dienste von hoher Qualität liefern. Formale Ansätze zur Verifikation solcher Systeme, wie z. B. Model Checking, sind aufgrund der extrem großen oder sogar unendlichen Zustandsräume, die diese Systeme besitzen, nur schwer anwendbar. Im Fall von Systemen mit unendlichen Zustandsraum werden viele interessante Verfikationsprobleme unentscheidbar, und traditionelle Model Checking Techniken für endliche Zustandsräume sind dann nicht mehr anwendbar.<br /><br />Wir schlagen ein auf ganzzahliger Programmierung beruhendes Gerüst zur Verifikation vor, welches auf der lokalen Analyse des zyklischen Verhaltens einer jeden Systemkomponente beruht. Dadurch vermeiden wir die Exploration des sehr großen oder sogar unendlichen Zustandsraums des Systems. Um genau zu sein, verwenden wir automatisierte Abstraktionstechniken, um ein zu analysierendes System in eine Menge von Kontrollflusszyklen zu überführen und den Nachrichten-Austauscheffekt dieser Zyklen zu überapproximieren. Für eine zu analysierende Eigenschaft bestimmen wir notwendige Bedingungen an die Kontrollflusszyklen, welche die Verletzung dieser Eigenschaft anzeigen. Diese Bedingungen werden dann in ein ganzzahliges Programmierungsproblem überführt, so dass dessen Lösungsraum das Eigenschaften verletzende Verhalten des Systems repräsentiert. Die Unlösbarkeit des ganzzahligen Programmierungsproblems beweist damit die Erfüllung der Eigenschaft durch das System. Das ganzzahlige Programmierungsproblem kann dann in polynomieller Zeit auf seine Lösbarkeit hin überprüft werden. Wir haben unser Verifikationsgerüst für die Verifikation der konkreten Eigenschaften der Beschränktheit von Kommunikationspuffern (boundedness of buffers) und der Abwesenheit von divergierendem Systemverhalten (absence of livelock) konkretisiert. Diese beiden Eigenschaften sind für asynchrone reaktive Systeme mit einem unendlichen Zustandsraum unentscheidbar.<br /><br />Dem gegenüber ist unser Verifikationsgerüst effizient, da es nicht alle exponentiell vielen linearisierten Ausführungsfolgen der Systemkomponenten betrachten muss. Es erhält die Lokalität der Analyse jeder einzelnen Systemkomponente und reduziert das ursprüngliche Verifikationsproblem zu einem Problem, das in polynomieller Zeit gelöst werden kann. Auf der anderen Seite ist unser Verifikationsgerüst unvollständig: es zeigt entweder die Erfüllung einer Eigenschaft, oder es endet mit einem untentschiedenen Verdikt, das wir mit UNKNOWN bezeichnen. In diesem Fall ist die Eigenschaft für das untersuchte System entweder erfüllt, oder nicht erfüllt. Diese Unschärfe wird durch die Grobheit der von unserem Verifikationsgerüst verwendeten Abstraktion hervorgerufen. Die Unvollständigkeit unseres Verfikationsgerüstes ist in jedem Fall unvermeidbar, da die überprüften Eigenschaften unentscheidbar sind.<br /><br />Da die Präzision unseres auf Abstraktion beruhenden Verifikationsgerüsts ein kritischer Punkt ist, schlagen wir automatische, auf Gegenbeispielen beruhende Abstraktionsverfeinerungsschritte vor. Diese beruhen auf der Entdeckung von Abhängigkeiten zwischen den Kontrollflusszyklen. Die entdeckten Abhängigkeiten können effizient in lineare Ungleichungen übersetzt werden, die dann dazu verwendet werden, die Menge der zur Lösung des ursprünglichen ILP Problems ermittelten linearen Ungleichungen zu erweitern. Die zusätzlichen Ungleichungen schließen möglicherweise nicht zulässiges Verhalten aus, welches zu einer Eigenschaftsverletzung führte, und verfeinern somit die ursprüngliche Abstraktion. Die Methoden zur Entdeckung von Zyklenabhängigkeiten sind ebenfalls unvollständig. Dies bedeutet, dass ein Teil des unzulässigen Verhaltens, das Eigenschaftsverletzungen zur Folge hat, möglicherweise durch die von uns entdeckten Zyklenabhängigkeiten nie entdeckt werden kann.<br /><br />Die resultierenden Verifikationsverfahren werden durch die Entwicklung von geeigneten Code-Abstraktionstechniken für zwei häufig verwendete Modellierungssprachen, nämlich Promela und UML RT, angepasst. Diese Techniken berücksichtigen spezifische Aspekte der beiden Sprachen, so besonders die Definition von Nachrichten, Prozessinstanziierungen, die Zuweisung von Nachrichtenpuffern, etc. Darüber hinaus haben wir eine automatische, unvollständige Methode zum Beweis der Termination von Programmschleifen entwickelt, welche ohne die explizite Konstruktion von Rangfolge-Funktionen auskommt. Schließlich haben wir mehrere Prototypen-Werkzeuge entwickelt, mit deren Hilfe wir viel versprechende experimentelle Resultate für reale Software-Modelle erhalten haben.</dcterms:abstract>
<dc:language>eng</dc:language>
<dc:rights>terms-of-use</dc:rights>
<dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T15:56:20Z</dcterms:available>
<dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/>
<void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
<dcterms:alternative>Unvollständige Eigenschaftsüberprüfung für Asynchrone Reaktive Systeme</dcterms:alternative>
<dcterms:title>Incomplete Property Checking for Asynchronous Reactive Systems</dcterms:title>
<foaf:homepage rdf:resource="http://localhost:8080/"/>
<dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T15:56:20Z</dc:date>
<dcterms:issued>2008</dcterms:issued>
<dc:creator>Wei, Wei</dc:creator>
<dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
<dc:contributor>Wei, Wei</dc:contributor>
<dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
<bibo:uri rdf:resource="http://kops.uni-konstanz.de/handle/123456789/5547"/>
<dc:format>application/pdf</dc:format>
<dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/5547/1/Diss_Wei.pdf"/>
<dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/5547/1/Diss_Wei.pdf"/>
</rdf:Description>
</rdf:RDF>
Internal note
xmlui.Submission.submit.DescribeStep.inputForms.label.kops_note_fromSubmitter
Examination date of dissertation
March 4, 2008