Embedded Systems: Challenges in Specification and Verification

In this position paper, we mention some of the challenges in specification and verification which are raised by the emerging discipline of embedded systems. The main proposition of the paper is that a feasible solution to the problem of effective, reliable, and dependable construction of embedded systems can be provided by a seamless development process based on a formal specification of the required system, which proceeds by the activities of verification and analysis of the specification at very early stages of the design, and then followed by automatic code generation, preceded if necessary by code distribution and allocation.As a prototype example of such a development process, we quote some experiences from the Sacres project and its follow-up Safeair. Necessary extensions to these preliminary experiments are discussed and evaluated.