Timing Verification of UML Activity Diagram Based Code Block Level Models for Real Time Multiprocessor System-on-Chip Applications

The UML activity diagram language is the de facto language for behavioral modeling capable of block level modeling of real time multiprocessor SoC applications where timing behavior is a critical aspect. Although there are several tools for timing verification of logics with branching time semantics, there are no known model checkers for timing verification of logics with linear time semantics as needed for many verification tasks. This work deals with timing verification of UML activity diagram models of applications. We propose a subset of TPTL (timed prepositional temporal logic) for specifying timing queries. We develop an automata based model checker for verifying such queries. We present a comparison of the proposed timing verification with the state of the art for random test-cases.