Modeling and verification of real-time embedded systems with urgency

Real-time embedded systems are often designed with different types of urgencies such as delayable or eager, that are modeled by several urgency variants of the timed automata model. However, most model checkers do not support such urgency semantics, except for the IF toolset that model checks timed automata with urgency against observers. This work proposes an Urgent Timed Automata (UTA) model with zone-based urgency semantics that gives the same model checking results as absolute urgency semantics of other existing urgency variants of the timed automata model, including timed automata with deadlines and timed automata with urgent transitions. A necessary and sufficient condition, called complete urgency, is formulated and proved for avoiding zone partitioning so that the system state graphs are simpler and model checking is faster. A novel zone capping method is proposed that is time-reactive, preserves complete urgency, satisfies all deadlines, and does not need zone partitioning. The proposed verification methods were implemented in the SGM CTL model checker and applied to real-time and embedded systems. Several experiments, comparing the state space sizes produced by SGM with that by the IF toolset, show that SGM produces much smaller state-spaces.     

VERTAF/Multi-Core: A SysML-Based Application Framework for Multi-Core Embedded Software Development

Multi-core processors are becoming prevalent rapidly in personal computing and embedded systems.Nevertheless,the programming environment for multi-core processor-based systems is still quite immature and lacks efficient tools.In this work,we present a new VERTAF/Multi-Core framework and show how software code can be automatically generated from SysML models of multi-core embedded systems.We illustrate how model-driven design based on SysML can be seamlessly integrated with Intel’s threading building blocks (TBB) and the quantum framework (QF) middleware.We use a digital video recording system to illustrate the benefits of the framework.Our experiments show how SysML/QF/TBB help in making multi-core embedded system programming model-driven,easy,and efficient.