Journal of Logic and Computation, Volume 11, Issue 6, pp. 829-878: Abstract.
Compositional Verification of Quantitative Properties of Statecharts
Dipartimento di Informatica, Corso Italia 40, Pisa, Italy. E-mail: email@example.com
In this paper we propose a process language JSP which abstractly models timed statecharts with minimal and maximal 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. Furthermore, we propose a compositional proof system to check quantitative temporal properties of statecharts processes. Properties are expressed 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).
Keywords: Timed statecharts, compositional verification, propositional µ, -, calculus, Local model checking