KOPS - Das Institutionelle Repositorium der Universität Konstanz

Integer linear programming-based property checking for asynchronous reactive systems

Integer linear programming-based property checking for asynchronous reactive systems


Dateien zu dieser Ressource

Prüfsumme: MD5:5827aeac42243d169d9f2a8006b013e0

LEUE, Stefan, Wei WEI, 2013. Integer linear programming-based property checking for asynchronous reactive systems. In: IEEE Transactions on Software Engineering. 39(2), pp. 216-236. ISSN 0098-5589

@article{Leue2013Integ-24347, title={Integer linear programming-based property checking for asynchronous reactive systems}, year={2013}, doi={10.1109/TSE.2011.1}, number={2}, volume={39}, issn={0098-5589}, journal={IEEE Transactions on Software Engineering}, pages={216--236}, author={Leue, Stefan and Wei, Wei} }

<rdf:RDF xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#" xmlns:bibo="http://purl.org/ontology/bibo/" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:dcterms="http://purl.org/dc/terms/" xmlns:xsd="http://www.w3.org/2001/XMLSchema#" > <rdf:Description rdf:about="https://kops.uni-konstanz.de/rdf/resource/123456789/24347"> <dc:contributor>Wei, Wei</dc:contributor> <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2013-09-11T08:55:19Z</dc:date> <dcterms:rights rdf:resource="http://nbn-resolving.org/urn:nbn:de:bsz:352-20140905103605204-4002607-1"/> <dc:contributor>Leue, Stefan</dc:contributor> <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2013-09-11T08:55:19Z</dcterms:available> <dc:creator>Wei, Wei</dc:creator> <dcterms:issued>2013</dcterms:issued> <dc:language>eng</dc:language> <bibo:uri rdf:resource="http://kops.uni-konstanz.de/handle/123456789/24347"/> <dcterms:abstract xml:lang="eng">Asynchronous reactive systems form the basis of a wide range of software systems, for instance in the telecommunications domain. It is highly desirable to rigorously show that these systems are correctly designed. However, traditional formal approaches to the verification of these systems are often difficult because asynchronous reactive systems usually possess extremely large or even infinite state spaces. We propose an integer linear program (ILP) solving-based property checking framework that concentrates on the local analysis of the cyclic behavior of each individual component of a system. We apply our framework to the checking of the buffer boundedness and livelock freedom properties, both of which are undecidable for asynchronous reactive systems with an infinite state space. We illustrate the application of the proposed checking methods to Promela, the input language of the SPIN model checker. While the precision of our framework remains an issue, we propose a counterexample guided abstraction refinement procedure based on the discovery of dependences among control flow cycles. We have implemented prototype tools with which we obtained promising experimental results on real-life system models.</dcterms:abstract> <dc:rights>deposit-license</dc:rights> <dcterms:title>Integer linear programming-based property checking for asynchronous reactive systems</dcterms:title> <dc:creator>Leue, Stefan</dc:creator> <dcterms:bibliographicCitation>IEEE transactions on software engineering ; 39 (2013), 2. - S. 216-236</dcterms:bibliographicCitation> </rdf:Description> </rdf:RDF>

Dateiabrufe seit 01.10.2014 (Informationen über die Zugriffsstatistik)

Leue_243472.pdf 271

Das Dokument erscheint in:

KOPS Suche


Mein Benutzerkonto