On the verification of SCOOP programs

Lade...
Vorschaubild
Dateien
Caltais_2-rw8j0pvgtud22.pdf
Caltais_2-rw8j0pvgtud22.pdfGröße: 451.91 KBDownloads: 395
Datum
2017
Autor:innen
Meyer, Bertrand
Herausgeber:innen
Kontakt
ISSN der Zeitschrift
Electronic ISSN
ISBN
Bibliografische Daten
Verlag
Schriftenreihe
Auflagebezeichnung
ArXiv-ID
Internationale Patentnummer
Angaben zur Forschungsförderung
Projekt
Open Access-Veröffentlichung
Open Access Green
Core Facility der Universität Konstanz
Gesperrt bis
Titel in einer weiteren Sprache
Forschungsvorhaben
Organisationseinheiten
Zeitschriftenheft
Publikationstyp
Zeitschriftenartikel
Publikationsstatus
Published
Erschienen 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.005
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)
004 Informatik
Schlagwörter
SCOOP; Operational semantics; Alias analysis; Deadlock detection; Rewriting logic
Konferenz
Rezension
undefined / . - undefined, undefined
Zitieren
ISO 690CALTAIS, 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.005
BibTex
@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>
Interner Vermerk
xmlui.Submission.submit.DescribeStep.inputForms.label.kops_note_fromSubmitter
Kontakt
URL der Originalveröffentl.
Prüfdatum der URL
Prüfungsdatum der Dissertation
Finanzierungsart
Kommentar zur Publikation
Allianzlizenz
Corresponding Authors der Uni Konstanz vorhanden
Internationale Co-Autor:innen
Universitätsbibliographie
Ja
Begutachtet
Diese Publikation teilen