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. Key words: Components, Real-time or embedded components, Component specification, Formal methods, Case study.

• Type: Journal
• Year: 2006
• Where: ENTCS
• Authors: Jan Carlson, John Håkansson, Paul Pettersson
• Keywords: Component Based Development, Embedded Systems, ENTCS 2006, Timed Automata