SaveCCM: An Analysable Component Model for Real-Time Systems

Component based development is a promising approach for embedded systems. Typical for embedded software is the presence of resource constraints in multiple dimensions. An essential dimension is time, since many embedded systems have real-time requirements. We define a formal semantics of a component language for embedded systems, SaveCCM, a language designed with vehicle applications and safety concerns in focus. The semantics is defined by a transformation into timed automata with tasks, a formalism that explicitly models timing and real-time task scheduling. A simple SaveCCM system with a PI controller is used as a case study. Temporal properties of the PI controller have been successfully verified using the timed automata model checker Uppaal.