On a Temporal Logic for Object-Based Systems

Dino Distefano; Joost-Pieter Katoen; Arend Rensink

doi:10.1007/978-0-387-35520-7_16

On a Temporal Logic for Object-Based Systems

Dino Distefano, Joost-Pieter Katoen, Arend Rensink

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

31 Citations (Scopus)

82 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 language	English
Title of host publication	Formal Methods for Open Object-Based Distributed Systems IV
Subtitle of host publication	IFIP TC6/WG6.1. Fourth International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS 2000) September 6–8, 2000, Stanford, California, USA
Editors	Scott F. Smith, Carolyn L. Talcott
Place of Publication	Boston, MA
Publisher	Kluwer Academic Publishers
Pages	305-326
Number of pages	22
ISBN (Electronic)	978-0-387-35520-7
ISBN (Print)	978-1-4757-1018-2
DOIs	https://doi.org/10.1007/978-0-387-35520-7_16
Publication status	Published - 2000
Event	4th IFIP TC6/WG6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems, FMOODS 2000 - Stanford, United States Duration: 6 Sept 2000 → 8 Sept 2000 Conference number: 4

Publication series

Name	IFIP Advances in Information and Communication Technology
Publisher	Kluwer Academic Publishers
Volume	10
ISSN (Print)	1868-4238
ISSN (Electronic)	1868-422X

Conference

Conference	4th IFIP TC6/WG6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems, FMOODS 2000
Abbreviated title	FMOODS
Country/Territory	United States
City	Stanford
Period	6/09/00 → 8/09/00

Keywords

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

Access to Document

10.1007/978-0-387-35520-7_16

Distefano00onAccepted author version, 163 KB

Cite this

Distefano, D., Katoen, J.-P., & Rensink, A. (2000). On a Temporal Logic for Object-Based Systems. In S. F. Smith, & C. L. Talcott (Eds.), Formal Methods for Open Object-Based Distributed Systems IV: IFIP TC6/WG6.1. Fourth International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS 2000) September 6–8, 2000, Stanford, California, USA (pp. 305-326). (IFIP Advances in Information and Communication Technology; Vol. 10). Kluwer Academic Publishers. https://doi.org/10.1007/978-0-387-35520-7_16

Distefano, Dino ; Katoen, Joost-Pieter ; Rensink, Arend. / On a Temporal Logic for Object-Based Systems. Formal Methods for Open Object-Based Distributed Systems IV: IFIP TC6/WG6.1. Fourth International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS 2000) September 6–8, 2000, Stanford, California, USA. editor / Scott F. Smith ; Carolyn L. Talcott. Boston, MA : Kluwer Academic Publishers, 2000. pp. 305-326 (IFIP Advances in Information and Communication Technology).

@inproceedings{a0330614dd594fcdb46a0d94a45bd98e,

title = "On a Temporal Logic for Object-Based Systems",

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.",

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

author = "Dino Distefano and Joost-Pieter Katoen and Arend Rensink",

year = "2000",

doi = "10.1007/978-0-387-35520-7_16",

language = "English",

isbn = "978-1-4757-1018-2",

series = "IFIP Advances in Information and Communication Technology",

publisher = "Kluwer Academic Publishers",

pages = "305--326",

editor = "Smith, {Scott F.} and Talcott, {Carolyn L.}",

booktitle = "Formal Methods for Open Object-Based Distributed Systems IV",

address = "Netherlands",

note = "4th IFIP TC6/WG6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems, FMOODS 2000, FMOODS ; Conference date: 06-09-2000 Through 08-09-2000",

}

Distefano, D, Katoen, J-P & Rensink, A 2000, On a Temporal Logic for Object-Based Systems. in SF Smith & CL Talcott (eds), Formal Methods for Open Object-Based Distributed Systems IV: IFIP TC6/WG6.1. Fourth International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS 2000) September 6–8, 2000, Stanford, California, USA. IFIP Advances in Information and Communication Technology, vol. 10, Kluwer Academic Publishers, Boston, MA, pp. 305-326, 4th IFIP TC6/WG6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems, FMOODS 2000, Stanford, California, United States, 6/09/00. https://doi.org/10.1007/978-0-387-35520-7_16

On a Temporal Logic for Object-Based Systems. / Distefano, Dino; Katoen, Joost-Pieter ; Rensink, Arend.
Formal Methods for Open Object-Based Distributed Systems IV: IFIP TC6/WG6.1. Fourth International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS 2000) September 6–8, 2000, Stanford, California, USA. ed. / Scott F. Smith; Carolyn L. Talcott. Boston, MA: Kluwer Academic Publishers, 2000. p. 305-326 (IFIP Advances in Information and Communication Technology; Vol. 10).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - On a Temporal Logic for Object-Based Systems

AU - Distefano, Dino

AU - Katoen, Joost-Pieter

AU - Rensink, Arend

N1 - Conference code: 4

PY - 2000

Y1 - 2000

N2 - 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.

AB - 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.

KW - FMT-MC: MODEL CHECKING

KW - Formal verification

KW - Object Constraint Language (OCL)

KW - Object-based system

KW - Property specification

KW - Temporal logic

U2 - 10.1007/978-0-387-35520-7_16

DO - 10.1007/978-0-387-35520-7_16

M3 - Conference contribution

SN - 978-1-4757-1018-2

T3 - IFIP Advances in Information and Communication Technology

SP - 305

EP - 326

BT - Formal Methods for Open Object-Based Distributed Systems IV

A2 - Smith, Scott F.

A2 - Talcott, Carolyn L.

PB - Kluwer Academic Publishers

CY - Boston, MA

T2 - 4th IFIP TC6/WG6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems, FMOODS 2000

Y2 - 6 September 2000 through 8 September 2000

ER -

Distefano D, Katoen JP , Rensink A. On a Temporal Logic for Object-Based Systems. In Smith SF, Talcott CL, editors, Formal Methods for Open Object-Based Distributed Systems IV: IFIP TC6/WG6.1. Fourth International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS 2000) September 6–8, 2000, Stanford, California, USA. Boston, MA: Kluwer Academic Publishers. 2000. p. 305-326. (IFIP Advances in Information and Communication Technology). doi: 10.1007/978-0-387-35520-7_16

On a Temporal Logic for Object-Based Systems

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this