Transactor-based Formal Verification of Real-time Embedded Systems

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 compoe described at high levels of abstraction, whereas others are described at low levels. Components in single ion level designs communicate through channels, which capture essential features of the communication. If the connected components communicate at different ion levels, then these channels are replaced with transactors that translate requests back and forth between raction 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.

• Type: Conference
• Year: 2007
• Where: FDL
• Authors: Daniel Karlsson, Petru Eles, Zebo Peng
• Keywords: FDL 2007, Ion Levels, Mixed Abstraction Levels, Natural Language Processing, Today's Embedded Systems