Abstract
The logic ATCTL is a convenient logic to specify properties with actions and real-time. It is intended as a property language for Lightweight UML models [12], which consist mainly of simplified class diagrams and statecharts. ATCTL combines two known extensions of CTL, namely ACTL and TCTL. The reason to extend CTL with both actions and real time is that in LUML state¿transition diagrams, we specify states, actions and real time, and our properties refer to all of these elements. The analyst therefore needs a property language that contains constructs for all these elements. ATCTL can be reduced to ACTL as well as to TCTL, and therefore also to CTL. This gives us a choice of tools for model checking; we have used is Kronos [13], a TCTL model checker.
| Original language | English |
|---|---|
| Number of pages | 8 |
| Publication status | Published - 2002 |
| Event | 5th IFIP TC6/WG6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems, FMOODS 2002 - Enschede, Netherlands Duration: 20 Mar 2002 → 22 Mar 2002 Conference number: 5 |
Conference
| Conference | 5th IFIP TC6/WG6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems, FMOODS 2002 |
|---|---|
| Abbreviated title | FMOODS |
| Country/Territory | Netherlands |
| City | Enschede |
| Period | 20/03/02 → 22/03/02 |