On a Temporal Logic for Object-Based Systems

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    26 Citations (Scopus)
    24 Downloads (Pure)

    Abstract

    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), an optional part of the UML standard for expressing static properties over class diagrams. 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.
    Original languageEnglish
    Title of host publicationFormal Methods for Open Object-Based Distributed Systems IV
    Subtitle of host publicationIFIP TC6/WG6.1. Fourth International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS 2000) September 6–8, 2000, Stanford, California, USA
    EditorsScott F. Smith, Carolyn L. Talcott
    Place of PublicationBoston, MA
    PublisherKluwer Academic Publishers
    Pages305-326
    Number of pages22
    ISBN (Electronic)978-0-387-35520-7
    ISBN (Print)978-1-4757-1018-2
    DOIs
    Publication statusPublished - 2000
    Event4th IFIP TC6/WG6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems, FMOODS 2000 - Stanford, United States
    Duration: 6 Sep 20008 Sep 2000
    Conference number: 4

    Publication series

    NameIFIP Advances in Information and Communication Technology
    PublisherKluwer Academic Publishers
    Volume10
    ISSN (Print)1868-4238
    ISSN (Electronic)1868-422X

    Conference

    Conference4th IFIP TC6/WG6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems, FMOODS 2000
    Abbreviated titleFMOODS
    CountryUnited States
    CityStanford
    Period6/09/008/09/00

    Keywords

    • FMT-MC: MODEL CHECKING
    • Formal verification
    • Object Constraint Language (OCL)
    • Object-based system
    • Property specification
    • Temporal logic

    Fingerprint Dive into the research topics of 'On a Temporal Logic for Object-Based Systems'. Together they form a unique fingerprint.

    Cite this