| Embedded and real-time systems are widely used in safety-critical areas such as aerospace, nuclear and traffic. Its scale becomes more complex, and architecture becomes more complicated. Therefore, verification and analysis for embedded and real-time systems become difficulties for academic and industry to overcome. UML, used to design software modeling, can't meet the demand of embedded and real-time systems modeling and lacks non-functional attributes modeling elements. The semi-formal models are difficult to be used for safety verification directly.To solve the problem, this thesis proposes a Sys ML activity diagram model with MARTE clock semantic information used for the safety verification for the embedded and real-time systems. The main contents are as follows:First, we use the Sys ML/MARTE activity diagram to model the embedded and real-time systems function, including Sys ML activity diagram modeling the function and the MARTE clock modeling the non-functional attributes. Then, we translate the Sys ML/MARTE activity diagram into timed automata based on metamodel, steps included:(1) according to modeling elements of Sys ML activity diagram and MARTE clock, build the metamodel of Sys ML activity diagram and MARTE clock, and combine the MARTE clock semantic information to Sys ML activity diagram, build the metamodel of timed automata;(2) give out the semantic mapping rules between metamodels of Sys ML/MARTE activity diagram and timed automata about types, behaviors and time elements; give out the structures transformation rules among them about nested, branch and concurrent structures; these can transform the Sys ML/MARTE activity diagram into timed automata;(3) convert the timed automaton into the textual timed automaton which can be read by model checker UPPAAL through grammar conversion. Last, according to the safety requirements of the embedded and real-time systems, extract the computation temporal logic and use UPPAAL to verify safety. |
PDF Full Text Request