On the verification of SCOOP programs

Cite This

Files in this item

Checksum: MD5:ca76e6e790b8f5e603de99729714f976

CALTAIS, Georgiana, Bertrand MEYER, 2017. On the verification of SCOOP programs. In: Science of Computer Programming. 133(2), pp. 194-215. ISSN 0167-6423. eISSN 1872-7964. Available under: doi: 10.1016/j.scico.2016.08.005

@article{Caltais2017-01verif-37783, title={On the verification of SCOOP programs}, year={2017}, doi={10.1016/j.scico.2016.08.005}, number={2}, volume={133}, issn={0167-6423}, journal={Science of Computer Programming}, pages={194--215}, author={Caltais, Georgiana and Meyer, Bertrand} }

<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/37783"> <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/37783/1/Caltais_2-rw8j0pvgtud22.pdf"/> <dcterms:issued>2017-01</dcterms:issued> <dc:creator>Caltais, Georgiana</dc:creator> <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/> <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/rdf/resource/123456789/36"/> <dcterms:rights rdf:resource="https://kops.uni-konstanz.de/page/termsofuse"/> <foaf:homepage rdf:resource="http://localhost:8080/jspui"/> <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2017-02-28T16:30:59Z</dc:date> <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2017-02-28T16:30:59Z</dcterms:available> <dc:rights>terms-of-use</dc:rights> <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/37783/1/Caltais_2-rw8j0pvgtud22.pdf"/> <dc:language>eng</dc:language> <bibo:uri rdf:resource="https://kops.uni-konstanz.de/handle/123456789/37783"/> <dc:creator>Meyer, Bertrand</dc:creator> <dcterms:abstract xml:lang="eng">In this paper we focus on the development of a unifying framework for the formal modeling of an object oriented-programming language, its underlying concurrency model and their associated analysis tools. More precisely, we target SCOOP – an elegant concurrency model, recently formalized based on Rewriting Logic (RL) and Maude. SCOOP is implemented in Eiffel and its applicability is demonstrated also from a practical perspective, in the area of robotics programming. Our contribution consists of devising and integrating an alias analyzer and a Coffman deadlock detector under the roof of the same RL-based semantic framework of SCOOP. This enables using the Maude rewriting engine and its LTL model-checker “for free,” in order to perform the analyses of interest. We discuss the limitations of our approach for model-checking deadlocks and provide possible workarounds for the state space explosion problem. On the aliasing side, we propose an extension of a previously introduced alias calculus based on program expressions, to the setting of unbounded program executions. Moreover, we devise a corresponding executable specification easily implementable on top of the SCOOP formalization. An important property of our extension is that, in non-concurrent settings, the corresponding alias expressions can be over-approximated in terms of a notion of regular expressions. This further enables us to derive an algorithm for computing a sound over-approximation of the “may aliasing” information, where soundness stands for the lack of false negatives.</dcterms:abstract> <dc:contributor>Caltais, Georgiana</dc:contributor> <dc:contributor>Meyer, Bertrand</dc:contributor> <dcterms:title>On the verification of SCOOP programs</dcterms:title> <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/rdf/resource/123456789/36"/> </rdf:Description> </rdf:RDF>

Downloads since Feb 28, 2017 (Information about access statistics)

Caltais_2-rw8j0pvgtud22.pdf 21

This item appears in the following Collection(s)

Search KOPS


Browse

My Account