Extending CTL with Actions and Real Time

Jansen, David N. and Wieringa, Roel J. (2002) Extending CTL with Actions and Real Time. Journal of Logic and Computation, 12 (4). pp. 607-621. ISSN 0955-792X

PDF
Restricted to UT campus only: Request a copy
173Kb

Abstract:	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.
Item Type:	Article
Copyright:	© 2002 Oxford University Press
Faculty:	Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:	Information Systems (IS)
Link to this item:	http://purl.utwente.nl/publications/38418
Official URL:	http://dx.doi.org/10.1093/logcom/12.4.607
Export this item as:	BibTeX EndNote HTML Citation Reference Manager

Show download statistics for this publication

Repository Staff Only: item control page

Metis ID: 210566