Variations of model checking

    Research output: Contribution to conferencePosterAcademic

    22 Downloads (Pure)

    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 languageEnglish
    Number of pages8
    Publication statusPublished - 2002
    Event5th IFIP TC6/WG6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems, FMOODS 2002 - Enschede, Netherlands
    Duration: 20 Mar 200222 Mar 2002
    Conference number: 5

    Conference

    Conference5th IFIP TC6/WG6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems, FMOODS 2002
    Abbreviated titleFMOODS
    Country/TerritoryNetherlands
    CityEnschede
    Period20/03/0222/03/02

    Fingerprint

    Dive into the research topics of 'Variations of model checking'. Together they form a unique fingerprint.

    Cite this