FORMAL VERIFICATION OF UML MARTE SPECIFICATIONS BASED ON A TRUE CONCURRENCY REAL TIME MODEL

摘要

For critical embedded systems the formal validation and verification is required. However, the real-time model checking suffers from problems of state-space explosion and clock explosion. The aim of this paper is to ensure an improvement of the Modeling and Analysis of Real-Time Embedded systems (MARTE), which is de facto standard, with formal semantics for verification finality. Therefore, we propose an operational method for translating UML sequence diagrams with MARTE annotations to Time Petri nets with Action Duration specifications (DTPN). Based on true concurrency semantics, the semantics of these specifications are defined in terms of Duration Action Timed Automata (daTA).