Linköping University: Students Alumni Trade and Industry/Society Internal Search

Transactor-based Formal Verification of Real-time Embedded Systems

Daniel Karlsson
Petru Eles Author homepage
Zebo Peng Author homepage

In Lecture Notes in Electrical Engineering, Vol. 10, Ed.: E. Villar, Springer.

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 chapter proposes a technique to generate such transactors. According to this technique, transRENCE on DIGITAL SYSTEM DESIGN (DSD 2008), Parma, Italy, September 3-5, 2008, pp. 71-80.In this paper we present an approach for scheduling with preemption for fault-tolerant embedded systems composed of soft and hard real-time processes. We are interested to maximize the overall utility for average, most likely to happen, scenarios and to guarantee the deadlines for the hard processes in the worst case scenarios. In many applications, the worst-case execution times of processes can be much longer than their average execution times. Thus, designs for the worst-case can be overly pessimistic, i.e., result in low overall utility. We propose preemption of process executions as a method to generate flexible schedules that maximize the overall utility for the average case while guarantee timing constraints in the worst case. Our scheduling algorithms determine off-line when to preempt and when to resurrect processes. The experimental results show the superiority of our new scheduling approach compared to approaches without preemption.

[KEP08] Daniel Karlsson, Petru Eles, Zebo Peng, "Transactor-based Formal Verification of Real-time Embedded Systems", In Lecture Notes in Electrical Engineering, Vol. 10, Ed.: E. Villar, Springer.
( ! ) perl script by Giovanni Squillero with modifications from Gert Jervan   (v3.1, p5.2, September-2002-)