Towards Model Checking OCL

D.S. Distefano; Joost P. Katoen; Arend Rensink

Towards Model Checking OCL

D.S. Distefano, Joost P. Katoen, Arend Rensink

Research output: Contribution to conference › Paper

1 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). 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 language	Undefined
Number of pages	10
Publication status	Published - 12 Jun 2000
Event	14th European Conference on Object-Oriented Programming, ECOOP 2000 - Sophia Antipolis and Cannes, France Duration: 12 Jun 2000 → 16 Jun 2000 Conference number: 14 http://users.polytech.unice.fr/~jpr/www-ecoop2000/

Conference

Conference	14th European Conference on Object-Oriented Programming, ECOOP 2000
Abbreviated title	ECOOP 2000
Country/Territory	France
City	Sophia Antipolis and Cannes
Period	12/06/00 → 16/06/00
Internet address	http://users.polytech.unice.fr/~jpr/www-ecoop2000/

Keywords

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

Access to Document

Cite this

@conference{c11d6b1e9c5a456c8b8ad2fd00b92d4f,

title = "Towards Model Checking OCL",

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

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

author = "D.S. Distefano and Katoen, {Joost P.} and Arend Rensink",

note = "Position paper; 14th European Conference on Object-Oriented Programming, ECOOP 2000 ; Conference date: 12-06-2000 Through 16-06-2000",

year = "2000",

month = jun,

day = "12",

language = "Undefined",

url = "http://users.polytech.unice.fr/~jpr/www-ecoop2000/",

}

TY - CONF

T1 - Towards Model Checking OCL

AU - Distefano, D.S.

AU - Katoen, Joost P.

AU - Rensink, Arend

N1 - Conference code: 14

PY - 2000/6/12

Y1 - 2000/6/12

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

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

KW - EWI-10041

KW - property specification

KW - Object Constraint Language (OCL)

KW - Temporal Logic

KW - object-based system

KW - Formal verification

KW - IR-61727

M3 - Paper

T2 - 14th European Conference on Object-Oriented Programming, ECOOP 2000

Y2 - 12 June 2000 through 16 June 2000

ER -