A Semantics of
Communicating Reactive Objects with Timing
and Mark van der Zwaag
Software Tools for Technology Transfer (STTT)
Volume 8, Number 4, pages 97-112, 2006.
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 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, i.e., a set of objects
which contains exactly one active object and where
at most one object may be executing.
Explicit timing is realized via local clocks and
an urgency predicate on transitions.
We define a formal semantics for this kernel language,
list a number of questions that arose, and
discuss the decisions taken.
The resulting semantics has been defined in the typed logic
of the interactive theorem prover
thus enabling formal verification based on this semantics.
Dump file of all PVS theories
version as Omega deliverabe
paper © Springer-Verlag