A dynamic verification method of executable UML/SysML models with timed-functional constraints

Abstract

We propose a dynamic method to verify system behaviors of executable models in UML/SysML. The verification checks timed-functional constraints as behavioral specification with the system's execution traces. Most of embedded/real-time system models consist of discrete behaviors of system controllers and continuous behaviors of mechanical/electronical systems. Therefore, the verification of discrete system behaviors using a static analysis technology like a model checking is inadequate for the verification of system overall behaviors, so that dynamic verification technologies are needed for developing embedded/real-time systems. Our verification method is effective for check satisfiability of non-functional requirements in early phase of development, e.g. performance requirements. The method verifies a event sequence captured as execution traces of the system model by checking with behavioral specification of event patterns specified in sequence diagrams with pre-conditions and constraints. A set of event patterns can be converted into a binary tree for quick verification with a large amount of execution traces.