The behavioural paradigm was proposed by professor W.M.Turski
as an alternative to the traditional computing paradigm. Behavioural programs
are reactive programs in which the actions are durative, that is, the state
in which the system is in at the time an action finishes execution is not
necessarily the same in which it was launched.
The behavioural paradigm is formalised here as a coordination
model between actions that modify a shared environment, that are durative
and that are likely to be heterogeneous as regards the programming language
in which they are given. This heterogeneity is possible due to the definition
of contexts, which constitute the interfaces of the actions. Coordination
is achieved through pre- and post-guards that establish criteria of activation/permission
for the execution and productivity of actions.
We present here a semantics for programs in the behavioural
paradigm in its three usual aspects: operational, denotational and axiomatic.
The rules of the operational semantics define a durative
transition system (std). This concept is introduced in this work with the
aim of generalising classical transition systems, in order to make it possible
to represent durative actions.
We define a durative transition logic (LTD) the formulas
of which are evaluated with respect to std-based models. The axiomatic
semantics is expressed in LTD. This logic, which is sound and complete,
allows us to express in a same formula the three states that characterise
a durative action: the launching, accepting and resulting states.
Several equivalence relations between behavioural programs
are presented that are based on bisimulation relations between stds. These
relations correspond to different points of view concerning what is considered
relevant in the execution of a program.
Behavioural properties of programs as, for example, stability,
reachability, deadlock freedom, are defined in an operational way through
restrictions to the std that is defined by the program and also in an axiomatic
way, through LTD formulas.