Lightweight Time Modeling in Timed Creol

TL;DR

This paper introduces a lightweight timed extension to the Creol modeling language, enabling better analysis of distributed systems with time-sensitive behaviors like message expiration and collision.

Contribution

It presents a novel, lightweight approach to incorporate time into Creol's semantics, enhancing its capability to model and analyze real-time distributed systems.

Findings

Timed semantics effectively model message expiration and collisions.

Implementation demonstrates practical analysis of radio communication systems.

Approach generalizes to other actor-based concurrent systems.

Abstract

Creol is an object-oriented modeling language in which inherently concurrent objects exchange asynchronous method calls. The operational semantics of Creol is written in an actor-based style, formulated in rewriting logic. The operational semantics yields a language interpreter in the Maude system, which can be used to analyze models. Recently, Creol has been applied to the modeling of systems with radio communication, such as sensor systems. With radio communication, messages expire and, if sent simultaneously, they may collide in the air. In order to capture these and other properties of distributed systems, we extended Creol's operational semantics with a notion of time. We exploit the framework of a language interpreter to use a lightweight notion of time, in contrast to that needed for a general purpose specification language. This paper presents a timed extension of Creol, including the semantics and the implementation strategy, and discusses its properties using an extended example. The approach can be generalized to other concurrent object or actor-based systems.