Transactor-based Formal Verification of Real-time Embedded Systems
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.
[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. |
|
