Towards Dependable Development Tools for Embedded Systems: A Case Study in Software Verification

Uwe Petermann, University of Applied Sciences Leipzig, Germany

This case study describes the specification and formal verification of the key part of TeCOM, a development tool for the design of open loop programmable control developed at the University of Applied Sciences in Leipzig. TeCOM translates the high-level representation of an open loop programmable control into a machine executable instruction list. The produced instruction list has to exhibit the same behavior as suggested by the high-level representation. We discuss the following steps of the case study: characterization of the correctness requirements, design of a verification strategy, and the correctness proof.


This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.