Embedded Software Design Methodology Based on Formal Models of Computation

Abstract

The current practice of embedded software design resorts to test or simulation to verify the correctness of the design, which is very time-consuming and incapable of covering all cases. Existent software engineering techniques are not concerned about real-time performance and resource requirements that embedded systems should satisfy for correct operation. In this work, we propose a new methodology to design dependable software for embedded systems. The key idea of the proposed methodology is to define a universal execution model (UEM) of heterogeneous multiprocessor embedded systems and to design the software based on the UEM that hides the underlying system architecture from the programmer. UEM puts restrictions on how to communicate and synchronize tasks that conventional operating systems deal with. We define the UEM by extending well-known formal models such as Synchronous Dataflow (SDF) and finite state machine (FSM). There are several benefits to use formal models for software design. First, we can detect critical design errors such as deadlock and buffer overflow by static analysis of formal models. Second, we can estimate the resource requirement and real-time performance at compile time. Last, not the least, we can synthesize the target code from the UEM automatically minimizing the manual coding efforts. By preserving the semantics of the UEM, the synthesized code will be correct by construction. The key challenge lies in the expression capability of the proposed UEM. Preliminary experiments with several non-trivial applications prove the viability of the proposed methodology.