danka_fdl07

Transactor-based Formal Verification of Real-time Embedded Systems

Daniel Karlsson Author homepage
 
Petru Eles Author homepage
Zebo Peng Author homepage

Forum on Specification & Design Languages (FDL), Barcelona, Spain, September 18-20, 2007.

ABSTRACT
With the increasing complexity of today’s embedded systems, there is a need to formally verify such designs at mixed abstraction levels. This is needed if some components are described at high levels of abstraction, whereas others are described at low levels. Components in single abstraction level designs communicate through channels, which capture essential features of the communication. If the connected components communicate at different abstraction levels, then these channels are replaced with transactors that translate requests back and forth between the abstraction levels. It is important that the transactor still preserves the external characteristics, e.g. timing, of the original channel. This paper proposes a technique to generate such transactors. According to this technique, transactors are specified in a single formal language, that is capable of capturing timing aspects. The approach is especially targeted to formal verification.


Related files:
danka_fdl07.pdfAdobe Acrobat portable document


[KEP07] Daniel Karlsson, Petru Eles, Zebo Peng, "Transactor-based Formal Verification of Real-time Embedded Systems", Forum on Specification & Design Languages (FDL), Barcelona, Spain, September 18-20, 2007.
( ! ) perl script by Giovanni Squillero with modifications from Gert Jervan   (v3.1, p5.2, September-2002-)
Last modified on Monday December 04, 2006 by Gert Jervan