Compositional Verification of Quantitative Properties of Statecharts

摘要

In this paper we propose a process language TSP which abstractly models timed statecharts with minimal and max- imal delays associated to transitions. Statecharts processes are equipped with a labelled transition system semantics that combines the basic principles of the semantics of Pnueli and Shalev with discrete time. Futhermore, we propose a composition proof system to check quantitative temporal properties of statecharts processes. Properties are ex- pressed in a discrete extension of μ-calculus with reset over clocks and clock constraints. The proof system is sound in general and it is complete for the class of regular processes (including processes corresponding to statecharts).