LotoTis and its Semantics
|
GMD Fokus
|
|
Hardenbergplatz 2
|
|
D-10623 Berlin
|
|
Germany
|
|
|
|
Tel: +30 254 99 241
|
|
Fax: +30 254 99 202
|
|
E-mail:
ina@fokus.gmd.de
|
Abstract:
LotoTis is a performance-oriented, upward compatible extension of LOTOS.
It is a proposal for enhancing LOTOS with
- quantified time,
- quantified nondeterminism (probabilistic behavior),
- quantified parallelism (resources), and
- action priorities.
LotoTis can describe
- the passage of time in between consecutive events,
- the weighted selection among different possible behavior, and
- the grade of parallelism within the specification.
Additionally, LotoTis offers a concept of monitoring that allows us to
derive any performance measure of interest from a LotoTis specification.
Structured actions are the central concept of LotoTis. Such a structured
action refines the notion of an action in classical process algebras
by a set of parameters which can be used to model real-time and other
performance-oriented aspects of system tasks. These parameters are the
interaction time, the action priority, the set of requested resources,
and the monitoring signal. Structured actions are in general
non-instantaneous, may overlap in time, and describe a true concurrent
behavior.
It is the use of resources that lead us to a new variant of the classical
as soon as possible paradigm: an action must occur as soon as it is enabled
and (!) the resources have been allocated. Let us notice that the
(unspecified) waiting periods for resources may extend to infinity. Thus,
minimal delays are specified by the duration of preceding hidden actions,
the duration of actions is modelled by non-zero interaction times, and last
but not least, maximal delays are described by the use of timeout
operators. It will be shown that LotoTis is equally expressive for the
description of time-critical behavior like other time proposals for
E-LOTOS. However, we argue that the basic LotoTis assumption of waiting as
long as necessary for resources and synchronization partners is the only
way to describe quantified parallelism by means of resources.
LotoTis is an upward compatible extension of LOTOS in two respects.
Every LOTOS specification is also a LotoTis specification with
equivalent semantics. Every LotoTis specification is a refinement of
its underlying LOTOS specification. Hence LotoTis supports for the
development of performance-oriented specification from existing LOTOS
specifications using a number of refinement rules.
After an introduction into LotoTis we will present its semantics. We use
the intermediate specification language GENIUS. GENIUS is an upward
compatible extension of LOTOS in the sense that it extends LOTOS with
additional features while preserving the original LOTOS semantics. GENIUS
has an operational semantics. LotoTis is transformed to GENIUS in order to
define the LotoTis semantics.
These two steps of semantics definition (from LotoTis to GENIUS, then
from GENIUS to SLTS) will be discussed. Afterwards, properties of LotoTis
are given.
This presentation has been given during the COST-247 4th Management Committee Meeting (Berlin, Germany, February 9--10, 1995).
COST-247 Working Group(s): 1-4
This Page was prepared by Mark Jorgensen.
Back to the VASY Home page
