On the verification of SCOOP programs
Dateien
Datum
Autor:innen
Herausgeber:innen
ISSN der Zeitschrift
Electronic ISSN
ISBN
Bibliografische Daten
Verlag
Schriftenreihe
Auflagebezeichnung
URI (zitierfähiger Link)
DOI (zitierfähiger Link)
Internationale Patentnummer
Link zur Lizenz
Angaben zur Forschungsförderung
Projekt
Open Access-Veröffentlichung
Sammlungen
Core Facility der Universität Konstanz
Titel in einer weiteren Sprache
Publikationstyp
Publikationsstatus
Erschienen in
Zusammenfassung
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.
Zusammenfassung in einer weiteren Sprache
Fachgebiet (DDC)
Schlagwörter
Konferenz
Rezension
Zitieren
ISO 690
CALTAIS, Georgiana, Bertrand MEYER, 2017. On the verification of SCOOP programs. In: Science of Computer Programming. 2017, 133(2), pp. 194-215. ISSN 0167-6423. eISSN 1872-7964. Available under: doi: 10.1016/j.scico.2016.08.005BibTex
@article{Caltais2017-01verif-37783,
year={2017},
doi={10.1016/j.scico.2016.08.005},
title={On the verification of SCOOP programs},
number={2},
volume={133},
issn={0167-6423},
journal={Science of Computer Programming},
pages={194--215},
author={Caltais, Georgiana and Meyer, Bertrand}
}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/37783">
<dc:creator>Meyer, Bertrand</dc:creator>
<dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2017-02-28T16:30:59Z</dc:date>
<dc:creator>Caltais, Georgiana</dc:creator>
<dcterms:issued>2017-01</dcterms:issued>
<dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
<dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2017-02-28T16:30:59Z</dcterms:available>
<dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/>
<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>
<void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
<bibo:uri rdf:resource="https://kops.uni-konstanz.de/handle/123456789/37783"/>
<dc:contributor>Caltais, Georgiana</dc:contributor>
<foaf:homepage rdf:resource="http://localhost:8080/"/>
<dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
<dcterms:title>On the verification of SCOOP programs</dcterms:title>
<dc:rights>terms-of-use</dc:rights>
<dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/37783/1/Caltais_2-rw8j0pvgtud22.pdf"/>
<dc:contributor>Meyer, Bertrand</dc:contributor>
<dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/37783/1/Caltais_2-rw8j0pvgtud22.pdf"/>
<dc:language>eng</dc:language>
</rdf:Description>
</rdf:RDF>
