You are here: Home / ECS / Research / Projects / CEVTES

CevTes - Project overview

The Project

 

 

News

July 2012
  • Our paper Real-Time Runtime Verification on Chip (co-authored with Matthias Függer and Jörg Brauer) has been accepted to RV'12. In this paper, we present an algorithmic framework that allows on-line motioning of past-time MTL specifications into efficient observer hardware blocks, which take advantage of the highly-parallel nature of hardware designs. For the time-bounded Since operator we get arrive at a time complexity that is double logarithmic in the time it is executed at and the given time bounds of the Since operator.
June 2012
  • Our paper A Runtime Verification Unit for Microcontrollers that we co-authored with Martin Horauer and Andreas Steininger, has been accepted to S4D'12. In this paper, we show an application of our runtime verification approach as watchdog replacement in microcontroller designs.
  • Andreas Hagmann (Vienna University of Technology) and Phillip Kadletz (University of Applied Sciences Technikum Wien) joined our team to work on their Master Theses. Welcome guys!
April 2012
  • Our paper Parallel Runtime Verification of Temporal Properties for Embedded Software that we co-authored with Johannes Geist, Patrick Moosbrugger, Martin Horauer and Andreas Steininger, has been accepted to MESA'12. In this paper, we extend our runtime verification framework to a highly parallel setting, that yields a close to linear speedup compared to a single core implementation.
August 2011
October 2011
August 2011
  • Our paper Automated Test-Trace Inspection for Microcontroller Binary Code that I co-authored with Jörg Brauer, Daniel Schachinger, Andreas Steininger and Stefan Kowalewski, has been accepted to RV'11. In this paper, we describe a non-intrusive framework for runtime verification of executable microcontroller code. The framework includes a custom-designed, resource friendly, microcontroller that evaluates ptLTL specification in parallel to program execution.
July 2011
  • Our paper Precise Control Flow Reconstruction Using Boolean Logic, co-authored with Jörg Brauer, our colleague from RWTH Aachen, has been accepted to EMSOFT'11. In this paper, we combine several techniques such as bit-blasting, Jörg's CAV'11 elimination algorithm and interleaved forward/backward analysis to compute fairly precise approximations of CFGs from binary code.
June 2011
  • Our workshop paper "Testing Microcontroller Software Simulators" was accepted for WS4C'11.
May 2011
  • Our paper "Past Time LTL Runtime Verification for Microcontroller Binary Code" was accepted for FMICS'11. In this paper, we show how to perform runtime verification for binary code without code instrumentation.
  • Our paper "Hardware Support for Efficient Testing of Embedded Software" was accepted for MESA'11. The aim of this work is a hardware unit that is (a) easily attachable to an off-the-shelf microcontroller IP-core and (b) allows to validate whether a property violation found by abstract interpretation of binary code also exhibits in a concrete run of the system.
November 2010
  • We have received a best paper award at MEMICS'10 for our paper "Test-Case Generation for Embedded Binary Code Using Abstract Interpretation".
September 2010
  • First results of the CevTes project will be presented at MEMCIS'10 Workshop in the paper "Test-Case Generation for Embedded Binary Code Using Abstract Interpretation".
August 2010
  • Tobias Müller, a student majoring Electronics at the University of Applied Sciences Technikum Wien, joined the project as a student member. He will be working on hardware implementations and concepts, crucial for ruling out infeasible test traces at the actual target hardware. 
July - August 2010
  • Thomas Reinbacher visited the Embedded Software Laboratory @ RWTH Aachen for a month, to collaborate on abstract interpretation techniques.

 

Introduction


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:

  • The problem to (manually) create a model of the system beforehand
  • The resulting large state spaces
  • Occurrence of false-negatives originating from the abstraction techniques applied

The novel approach presented in the CevTes project focuses on the development of a hardware framework to assist assembly code model checking and abstract interpretation. The innovation targets:

  • Automatic validation of counterexamples
  • Abstraction techniques supporting binary code analysis
  • Automated test case generation
  • Automated execution of these test cases within the target environment

Herein, CevTes focuses on ruling out false-negatives by cross-checking error traces on the real target platform (i.e., a customized microcontroller IP-core), reducing the state explosion problem for assembly code model checking in particular, and address the problem of creating test cases for tests such as acceptance tests of embedded software. 

 

Project Aims


The fundamental milestones of the project are:

  • System architecture for microcontroller IP cores to support test case generation and test case / counterexample execution within the target platform
  • A test case generation approach for embedded systems software based on binary code analysis through static analysis, abstract interpretation and model checking

Publications

Reviewed conference papers

 

 

Participating Organizations & People



(Student) Team Members


 


 


 


 


 


 

Acknowledgements