Home  Online Resources  Table of Contents

Journal of Logic and Computation, Volume 11, Issue 6, pp. 829-878: Abstract.

Compositional Verification of Quantitative Properties of Statecharts

Francesca Levi

Dipartimento di Informatica, Corso Italia 40, Pisa, Italy. E-mail: levifran@di.unipi.it

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

  Full-Text PDF  (579 KB)

[ Oxford University Press]   [ Oxford Journals]   [ Comments & Feedback]   Copyright© Oxford University Press, 2001.