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

[img] PDF
Restricted to UT campus only
: Request a copy
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
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/38418
Official URL:https://doi.org/10.1093/logcom/12.4.607
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page

Metis ID: 210566