Demo abstract: Platform dependent code generation of real-time embedded software

Embedded software constitutes an important part of modern safety-critical systems, such as medical devices. As embedded software is increasingly complex, assuring the safety of such software becomes difficult, especially when the correct function is highly dependent on stringent timing and memory constraints of the implementation platform. Model-based development methodology has garnered attentions as an effective method for creating safety-critical embedded software in a systematic way, so that high-level safety assurance is guaranteed in the final implemented systems. In this methodology, the software system is first modeled using an abstract model, such as timed-automata, which can then be verified using a formal verification tool, such as UPPAAL. Then, code-generation techniques are applied to automatically generate source code from the verified model.