TU Darmstadt / ULB / TUbiblio

Automated model extraction: From non-deterministic C code to active objects

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, Elsevier, ISSN 0167-6423,
DOI: 10.1016/j.scico.2020.102597,
[Article]

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.

Item Type: Article
Erschienen: 2021
Creators: Wasser, Nathan ; Tabar, Asmae Heydari ; Hähnle, Reiner
Title: Automated model extraction: From non-deterministic C code to active objects
Language: English
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.

Journal or Publication Title: Science of Computer Programming
Volume of the journal: 204
Publisher: Elsevier
Divisions: 20 Department of Computer Science
20 Department of Computer Science > Software Engineering
Date Deposited: 19 Jul 2022 08:35
DOI: 10.1016/j.scico.2020.102597
Additional Information:

Art.No.: 102597

PPN:
Export:
Suche nach Titel in: TUfind oder in Google
Send an inquiry Send an inquiry

Options (only for editors)
Show editorial Details Show editorial Details