Refinement-Based Verification of Communicating Unstructured Code
| dc.contributor.author | Jähnig, Nils | |
| dc.contributor.author | Göthel, Thomas | |
| dc.contributor.author | Glesner, Sabine | |
| dc.date.accessioned | 2020-03-09T09:10:24Z | |
| dc.date.available | 2020-03-09T09:10:24Z | |
| dc.date.issued | 2016-06-23 | |
| dc.description.abstract | Formal model refinement aims at preserving safety and liveness properties of models. However, there is usually a verification gap between model and executed code, especially if concurrent processes are involved. The reason for this is that a manual implementation and further code optimizations can introduce implementation errors. In this paper, we present a framework that allows for formally proving a failures refinement between a CSP specification and its low-level implementation. The implementation is given in a generic unstructured language with gotos and an abstract communication instruction. We provide a failures-based denotational semantics of it with an appropriate Hoare calculus. Since failures-based refinement is compositional w.r.t. parallel composition of concurrent components and preserves safety and liveness properties, this contributes to reducing the verification gap between high-level specifications and their low-level implementations. | en |
| dc.identifier.eissn | 1611-3349 | |
| dc.identifier.isbn | 978-3-319-41590-1 | |
| dc.identifier.isbn | 978-3-319-41591-8 | |
| dc.identifier.issn | 0302-9743 | |
| dc.identifier.uri | https://depositonce.tu-berlin.de/handle/11303/10899 | |
| dc.identifier.uri | http://dx.doi.org/10.14279/depositonce-9792 | |
| dc.language.iso | en | en |
| dc.rights.uri | http://rightsstatements.org/vocab/InC/1.0/ | en |
| dc.subject.ddc | 005 Computerprogrammierung, Programme, Daten | de |
| dc.subject.other | gotos | en |
| dc.subject.other | unstructured code | en |
| dc.subject.other | formal semantics | en |
| dc.subject.other | Hoare calculus | en |
| dc.subject.other | CSP | en |
| dc.subject.other | failures refinement | en |
| dc.title | Refinement-Based Verification of Communicating Unstructured Code | en |
| dc.type | Conference Object | en |
| dc.type.version | acceptedVersion | en |
| dcterms.bibliographicCitation.doi | 10.1007/978-3-319-41591-8_5 | en |
| dcterms.bibliographicCitation.originalpublishername | Springer | |
| dcterms.bibliographicCitation.originalpublisherplace | Cham | |
| dcterms.bibliographicCitation.pageend | 75 | en |
| dcterms.bibliographicCitation.pagestart | 61 | en |
| dcterms.bibliographicCitation.proceedingstitle | SEFM 2016: Software Engineering and Formal Methods | en |
| tub.accessrights.dnb | free | en |
| tub.affiliation | Fak. 4 Elektrotechnik und Informatik::Inst. Softwaretechnik und Theoretische Informatik | de |
| tub.affiliation.faculty | Fak. 4 Elektrotechnik und Informatik | de |
| tub.affiliation.institute | Inst. Softwaretechnik und Theoretische Informatik | de |
| tub.publisher.universityorinstitution | Technische Universität Berlin | en |
| tub.series.issuenumber | 9763 | en |
| tub.series.name | Lecture Notes in Computer Science | en |