13th Asia Pacific Software Engineering Conference (APSEC'06)
Timing Verification of UML Activity Diagram Based Code Block Level Models for Real Time Multiprocessor System-on-Chip Applications
Bangalore, India
December 06-December 08
ISBN: 0-7695-2685-3
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 Propositional 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 testcases.
Citation:
Dipankar Das, Rajeev Kumar, P. P. Chakrabarti, "Timing Verification of UML Activity Diagram Based Code Block Level Models for Real Time Multiprocessor System-on-Chip Applications," apsec, pp.199-208, 13th Asia Pacific Software Engineering Conference (APSEC'06), 2006