Variations of model checking

D.N. Jansen

    Research output: Contribution to conferencePosterAcademic

    4 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
    CountryNetherlands
    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