%%%% ABSTRACT %%%%
The aim of this work is to provide a formal
foundation for the unambiguous description of
real-time, reactive, embedded systems in UML.
For this application domain, we define the
meaning of basic class diagrams where the
behavior of objects is described by
timed state machines.
These reactive objects may communicate
by means of asynchronous
signals and synchronous operation calls.
The notion of a thread of control is captured by
a so-called activity group, which is a set of objects
which contains exactly one active object and where
at most one object may be executing.
We define a formal semantics for this kernel language,
based on the run-to-completion paradigm.
We show that this combination of communication primitives and
execution mechanism gives rise to a large number of
questions and list the decisions taken in the proposed
semantics.
The resulting semantics is defined in the typed logic
of the interactive theorem prover PVS.