On the verification of SCOOP programs

Cite This

Files in this item

Files Size Format View

There are no files associated with this item.

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"> <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"/> <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: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> <dcterms:title>On the verification of SCOOP programs</dcterms:title> <dc:contributor>Meyer, Bertrand</dc:contributor> <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/rdf/resource/123456789/36"/> </rdf:Description> </rdf:RDF>

This item appears in the following Collection(s)

Search KOPS


My Account