Algebra of Communicating Shared Resources
The Algebra of Communicating Shared Resources, ACSR, is a timed
process algebra that is based on the premise that the timed behavior
of a real-time system is affected not only by the time its components
take to execute and synchronize, but also by delays introduced due to
the scheduling of actions that compete for shared resources.
The ACSR computation model is based on the view that the components of
a real-time system execute synchronously time and resource consuming
actions and communicate through instantaneous events asynchronously,
except when two components synchronize through matching events. To be
able to specify real-time systems accurately, ACSR supports static
priorities that can be used to arbitrate between actions competing for
shared resources and between events that are ready for
synchronization. ACSR also offers different notions of equivalence
that can be used to verify that two specifications behave the same.
ACSR has been implemented within the VERSA
[CLX95]
toolkit which has three major functions: rewriting, equivalence
testing, and interactive execution. We have found that VERSA greatly
facilitates the task of using ACSR for non-trivial examples through
computer assistance for checking syntax and carrying out analysis
automatically.
Graphical Communicating Shared Resources
Graphical Communicating Shared Resources, GCSR, is a formal language for the
specification, refinement, and analysis of real-time systems
[RTSS'95,
Tech Report,
Dissertation proposal].
GCSR graphical notation is selected to produce unambiguous, scalable
descriptions of real-time systems. GCSR allows the integration of a
system functional requirements (e.g., concurrent execution,
communication, timing constraints, etc.) together with its resource
requirements (e.g., cpu, memory, sensors, etc.). The semantics of
GCSR is defined through a precise translation to the Algebra of
Communicating Shared Resources, ACSR.
To support the top-down development of real-time systems, GCSR
provides notions of refinement that allow a designer to describe a
system at an abstract level. At this level, a designer may estimate
the resource requirements. They can later add more details to the
abstract specification by showing the internal structure of a
component, explicitly presenting local communications, and tightening
the resource requirements. The semantics of the refinements is
defined in terms of trace ordering relations with essential properties
such as preservation of the timed occurrences of events.
Analysis within the GCSR formalism is supported through execution of a
GCSR specification and automated verification of the equivalence of
specifications (e.g., requirements and design). Execution of a GCSR
specification is supported through the precise correspondence between
GCSR and ACSR and the operational semantics of ACSR. Equivalence
checking is supported through the various notions of equivalence in
ACSR.
We are currently implementing a graphical user interface where GCSR
specifications can be drawn, syntax-checked, refined, and analyzed.
Communicating Timed State Machines
Communicating Timed State Machines,
CTSM,
is a formal model for describing real-time systems.
In CTSM, a system consists of concurrent processes communicating
with each other through channels. Each process has data variables
with arbitrary domain and clock variables with dense domain, where
clock variables are special variables used to express various timing
constraints such as delays and deadlines.
CTSMs are compositional; that is, a CTSM process can
be constructed by composing two CTSM processes.