OceanRep
MEMICS - Memory Interval Constraint Solving of (concurrent) Machine Code.
Nowotka, Dirk and Traub, Johannes (2012) MEMICS - Memory Interval Constraint Solving of (concurrent) Machine Code. [Paper] In: Automotive - Safety & Security. , 14-15 Nov 2012, Karlsruhe, Germany . Automotive - Safety & Security 2012. ; pp. 69-84 . Lecture Notes in Informatics, P-210 .
Preview |
Text
MEMICS.pdf Download (235kB) | Preview |
Abstract
Runtimeerrorsoccurringirregularlyinautomotivecontrolunitsareoftenhardtodetect.Acommonreason for such errors are critical race conditions. The introduction of multicore hardware enables software to be run in parallel, and hence, drastically increases the vulnerability to such errors. Race conditions are difficult to discover by testing or monitoring, only. Additionally, a static analysis of code is required to effectively reduce the occurrence of such errors. In this paper we introduce a new Bounded Model Checking tool, which in its core is an Interval Constraint Solver, operating on a machine code based model and is able to handle memory instructions directly. As control units are usually running on task-based operating systems like AUTOSAR or OSEK, our tool features a task model, which is able to handle sequential and concurrent task scheduling.
Document Type: | Conference or Workshop Item (Paper) |
---|---|
Keywords: | formal verification concurrent code interval constraint solving |
Research affiliation: | Kiel University |
Publisher: | Gesellschaft für Informatik |
Date Deposited: | 21 Jan 2013 19:48 |
Last Modified: | 23 Sep 2019 23:56 |
URI: | https://oceanrep.geomar.de/id/eprint/20172 |
Actions (login required)
View Item |
Copyright 2023 | GEOMAR Helmholtz-Zentrum für Ozeanforschung Kiel | All rights reserved
Questions, comments and suggestions regarding the GEOMAR repository are welcomed
at bibliotheksleitung@geomar.de !