Oxford Journals
tools journals homepage advanced search contact help
Journal of Logic and Computation: Current Issue

OUP > Journals > Computing/Engineer. & Mathematics/Stats. > Journal of Logic and Computation

Journal of Logic and Computation

Volume 12, Issue 4, August 2002: pp. 607-621

Extending CTL with Actions and Real Time

David N. Jansen1 and Roel J. Wieringa1

1Universiteit Twente, Faculteit der Informatica, Vakgroep IS, Postbus 217, NL-7500 AE Enschede, The Netherlands. E-mail: dnjansen@cs.utwente.nl, roelw@cs.utwente.nl

In this paper, we present the logic ATCTL, which is intended to be used for model checking models that have been specified in a lightweight version of the Unified Modelling Language (UML). Elsewhere, we have defined a formal semantics for LUML to describe the models. This paper's goal is to give a specification language for properties that fits LUML; LUML includes states, actions and real time. ATCTL extends CTL with concurrent actions and real time. It is based on earlier extensions of CTL by De Nicola and Vaandrager (ACTL) and Alur et al. (TCTL). This makes it easier to adapt existing model checkers to ATCTL. To show that we can check properties specified in ATCTL in models specified in LUML, we give a small example using the Kronos model checker.

Keywords: Real-time logic; model checking; action modalities

Table of Contents   Full-Text PDF (173 KB)

Oxford University Press
Published by Oxford University Press
Copyright ©Oxford University Press 2003
Print ISSN: 0955-792X  Online ISSN: 1465-363X.
Oxford University Press Privacy Policy and Legal Statement