KOPS - Das Institutionelle Repositorium der Universität Konstanz

Directed explicit state-space search in the generation of counterexamples for stochastic model checking

Directed explicit state-space search in the generation of counterexamples for stochastic model checking

Zitieren

Dateien zu dieser Ressource

Dateien Größe Format Anzeige

Zu diesem Dokument gibt es keine Dateien.

ALJAZZAR, Husain, Stefan LEUE, 2010. Directed explicit state-space search in the generation of counterexamples for stochastic model checking. In: IEEE Transactions on Software Engineering. 36(1), pp. 37-60. ISSN 0098-5589. Available under: doi: 10.1109/TSE.2009.57

@article{Aljazzar2010Direc-3015, title={Directed explicit state-space search in the generation of counterexamples for stochastic model checking}, year={2010}, doi={10.1109/TSE.2009.57}, number={1}, volume={36}, issn={0098-5589}, journal={IEEE Transactions on Software Engineering}, pages={37--60}, author={Aljazzar, Husain and Leue, Stefan} }

<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/rdf/resource/123456789/3015"> <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/rdf/resource/123456789/36"/> <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/rdf/resource/123456789/36"/> <dc:rights>deposit-license</dc:rights> <dcterms:issued>2010</dcterms:issued> <dc:creator>Aljazzar, Husain</dc:creator> <dcterms:rights rdf:resource="http://nbn-resolving.org/urn:nbn:de:bsz:352-20140905103416863-3868037-7"/> <dc:creator>Leue, Stefan</dc:creator> <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-23T10:15:46Z</dc:date> <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-23T10:15:46Z</dcterms:available> <dcterms:bibliographicCitation>First publ. in: IEEE Transactions on Software Engineering 36 (2010), 1, pp. 37-60</dcterms:bibliographicCitation> <dc:contributor>Aljazzar, Husain</dc:contributor> <dcterms:abstract xml:lang="eng">Current stochastic model checkers do not make counterexamples for property violations readily available. In this paper, we apply directed explicit state-space search to discrete and continuous-time Markov chains in order to compute counterexamples for the violation of PCTL or CSL properties. Directed explicit state-space search algorithms explore the state space on-the-fly, which makes our method very efficient and highly scalable. They can also be guided using heuristics which usually improve the performance of the method. Counterexamples provided by our method have two important properties. First, they include those traces which contribute the greatest amount of probability to the property violation. Hence, they show the most probable offending execution scenarios of the system. Second, the obtained counterexamples tend to be small. Hence, they can be effectively analyzed by a human user. Both properties make the counterexamples obtained by our method very useful for debugging purposes. We implemented our method based on the stochastic model checker PRISM and applied it to a number of case studies in order to illustrate its applicability.</dcterms:abstract> <dcterms:title>Directed explicit state-space search in the generation of counterexamples for stochastic model checking</dcterms:title> <bibo:uri rdf:resource="http://kops.uni-konstanz.de/handle/123456789/3015"/> <dc:language>eng</dc:language> <foaf:homepage rdf:resource="http://localhost:8080/jspui"/> <dc:contributor>Leue, Stefan</dc:contributor> <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/> </rdf:Description> </rdf:RDF>

Das Dokument erscheint in:

KOPS Suche


Stöbern

Mein Benutzerkonto