Wasser, Nathan ; Tabar, Asmae Heydari ; Hähnle, Reiner (2021)
Automated model extraction: From non-deterministic C code to active objects.
In: Science of Computer Programming, 204
doi: 10.1016/j.scico.2020.102597
Artikel, Bibliographie
Kurzbeschreibung (Abstract)
The C programming language is well-known to have a large amount of underspecified behavior that often results in non-determinism even of sequential programs. In many application areas, not necessarily safety-critical ones, this is highly undesirable. A number of approaches and tools that statically analyze such behavior have been suggested, but they suffer from a high number of false positives and negatives. We present a novel model-based approach to analyzing non-determinism that works by automatic extraction of a faithful model of a given C program in a concurrent active object language. The extracted model renders any non-deterministic behavior of the C program in terms of explicit concurrency. This opens the door to global, semantic analyses. We give a fully formal account of the model extraction process and present an experimental evaluation of its implementation in the model extraction tool C2ABS.
| Typ des Eintrags: | Artikel |
|---|---|
| Erschienen: | 2021 |
| Autor(en): | Wasser, Nathan ; Tabar, Asmae Heydari ; Hähnle, Reiner |
| Art des Eintrags: | Bibliographie |
| Titel: | Automated model extraction: From non-deterministic C code to active objects |
| Sprache: | Englisch |
| Publikationsjahr: | 1 April 2021 |
| Verlag: | Elsevier |
| Titel der Zeitschrift, Zeitung oder Schriftenreihe: | Science of Computer Programming |
| Jahrgang/Volume einer Zeitschrift: | 204 |
| DOI: | 10.1016/j.scico.2020.102597 |
| Kurzbeschreibung (Abstract): | The C programming language is well-known to have a large amount of underspecified behavior that often results in non-determinism even of sequential programs. In many application areas, not necessarily safety-critical ones, this is highly undesirable. A number of approaches and tools that statically analyze such behavior have been suggested, but they suffer from a high number of false positives and negatives. We present a novel model-based approach to analyzing non-determinism that works by automatic extraction of a faithful model of a given C program in a concurrent active object language. The extracted model renders any non-deterministic behavior of the C program in terms of explicit concurrency. This opens the door to global, semantic analyses. We give a fully formal account of the model extraction process and present an experimental evaluation of its implementation in the model extraction tool C2ABS. |
| Zusätzliche Informationen: | Art.No.: 102597 |
| Fachbereich(e)/-gebiet(e): | 20 Fachbereich Informatik 20 Fachbereich Informatik > Software Engineering |
| Hinterlegungsdatum: | 19 Jul 2022 08:35 |
| Letzte Änderung: | 20 Jul 2022 07:38 |
| PPN: | |
| Export: | |
| Suche nach Titel in: | TUfind oder in Google |
 |
Frage zum Eintrag |
Optionen (nur für Redakteure)
 |
Redaktionelle Details anzeigen |
Drucken
Impressum