CounterExample Validation and Test Case Generation Framework for Verifiying Embedded Software

01.04.2010 - 30.09.2013
Research funding project
Verification and validation of embedded systems software is crucial for providing flawless functionality of nowadays intelligent computer systems found in automobiles, elevators, aircrafts, medical devices, robots, etc. The common approach most widely used in industry relies on testing of defined corner cases. Although everyone is aware of the fact that only a very limited set of the test space can be covered in this way, no other more complete approaches have been adopted so far. Formal verification methods such as model checking complemented with various techniques to reduce state spaces have recently gained some momentum in this regard. Nevertheless, formal verification of embedded systems still plays a minor role. Practical restrictions of this approach are (i) the problem to (manually) create a model of the system beforehand, (ii) the resulting large state spaces, and (iii) the occurrence of false-negatives originating from the abstraction techniques applied. The novel approach presented in this project focuses on the development of a hardware framework to support assembly code model checking and static analysis. The innovation targets (a) automatic validation of counterexamples, (b) counterexample guided abstraction refinement, (c) automated test case generation, and (d) automated execution of these test cases within the target environment. Herein (a) focuses on ruling out false-negatives by cross-checking error traces on the real target platform (i.e., a customized microcontroller IP-core), (b) helps to reduce the state explosion problem for assembly code model checking in particular, and (c+d) address the problem of creating test cases for tests such as acceptance tests of embedded software.

People

Project leader

Project personnel

Institute

Grant funds

  • FFG - Österr. Forschungsförderungs- gesellschaft mbH (National) Austrian Research Promotion Agency (FFG)

Research focus

  • Computer Engineering: 100%

Keywords

GermanEnglish
Counterexample-Validierungcounterexample validation
Testfallgenerierungtest case generation
statische Analyse und Modelchecking von Assemblercodeassembly code static analysis and modelchecking
formale Verifikationformal verification
eingebettete Softwareembedded systems software

External partner

  • RWTH Aachen
  • FH Technikum Wien

Publications