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 toolkit and PARAGON toolset.
VERSA [CLX95] 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.
PARAGON provides a visual, process algebraic design environment for real-time systems.




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]. 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 either directly as a labeled transition system or indirectly through a precise translation to the Algebra of Communicating Shared Resources (ACSR). The graphical notation of GCSR is selected to produce unambiguous, scalable descriptions of real-time systems.

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 estimate 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.

GCSR has been implemented within PARAGON, an environment for the visual, top-down design and analysis of real-time systems.




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.