A Formal Approach for Analysis and Testing of Reliable Embedded Systems

In this paper, a framework for the specification of embedded systems described as 'predicated' extended finite state machines (p-EFSMs) is proposed. Compared to simple FSMs, p-EFSMs allow the control flow and the data flow description of hardware modules or software processes. We introduce a new variant of the EFSM model, a so-called 'predicated' EFSM that extends the usual EFSM. This extension offers a more convenient mean to specify constraints on the system's transitions. Secondly, it provides an easy mapping onto formal description techniques. Thirdly, it allows the development of an embedded system independently from the implementation, i.e. without favoring a hardware or a software. Crucial tasks in the design of reliable embedded systems are analysis and testing. These allow the system developer to detect bugs that may be very costly to do in subsequent phases of the system development. We identify the different testing issues and demonstrate how the bugs can be detected by means of p-EFSMs. Failure detection and elimination improve the likelihood of the well-functioning and the reliability of the embedded system.