Towards Model Checking OCL

    Research output: Contribution to conferencePaper

    1 Downloads (Pure)


    This paper presents a logic, called BOTL (Object-Based Temporal Logic), that facilitates the specification of dynamic and static properties of object-based systems. The logic is based on the branching temporal logic CTL and the Object Constraint Language (OCL). Eventually, the aim is to do model checking. The formal semantics of BOTL is defined in terms of a general operational model that is aimed to be applicable to a wide range of object-oriented languages. A mapping of a large fragment of OCL onto BOTL is defined, thus providing a formal semantics to OCL and, at the same time, permitting model checking of OCL constraints.
    Original languageUndefined
    Number of pages10
    Publication statusPublished - 12 Jun 2000
    Event14th European Conference on Object-Oriented Programming, ECOOP 2000 - Sophia Antipolis and Cannes, France
    Duration: 12 Jun 200016 Jun 2000
    Conference number: 14


    Conference14th European Conference on Object-Oriented Programming, ECOOP 2000
    Abbreviated titleECOOP 2000
    CitySophia Antipolis and Cannes
    Internet address


    • EWI-10041
    • property specification
    • Object Constraint Language (OCL)
    • Temporal Logic
    • object-based system
    • Formal verification
    • IR-61727

    Cite this