Graphical Communicating Shared Resources: A Language for the Specification, Refinement, and Analysis of Real-Time Systems

The Communicating Shared Resources (CSR) paradigm is an ongoing project at the University of Pennsylvania to build a framework for the development of real-time systems. This project has been motivated by a demand for a rigorous framework in which various design alternatives for a real-time system can be formally specified and rigorously analyzed and tested before implementation. This is an effort to reduce the potentially high cost associated with incorrect operation of real-time systems which are often embedded in safety-critical applications. The work presented in this thesis is a first step towards incorporating software engineering practices into the CSR paradigm. This is achieved, on one hand, by developing a formal, graphical CSR formalism, the Graphical Communicating Shared Resources (GCSR); the GCSR language adopts the intuitive concepts of nodes and edges in state diagrams, an informal specification language that is popular within the software engineering community. In addition, defining a refinement theory for GCSR allows the development of real-time systems within this formalism in a top-down and modular fashion, also a popular design methodology within the software engineering community. The GCSR language adopts a syntax that allows a modular and hierarchical, thus, scalable description of a real-time system. It supports notions of comunication through events, interrupt, concurrency, and time to describe the functional and temporal requirements of a real-time system. In addition, GCSR allows the explicit representation of resources and priorities to resolve resource contention, in such a way that produces easy to understand and modify specifications. The semantics of GCSR is defined operationally either through a direct translation of a GCSR description to a labeled transition system, or indirectly through a sound translation to the Algebra of Communicating Shared Resources (ACSR) [LBGG94] a timed process algebra that also has an operational semantics. The GCSR-ACSR correspondence makes GCSR benefit from process algebraic analysis techniques such as equivalence checking, state space exploration, testing as well as simulation. In addition, the tight correspondence between GCSR and ACSR makes it possible to use the graphical and textual notations interchangeably and to have a sound theory for graphical transformation operations, e.g., to minimize the number of edges and nodes in a GCSR specification without affecting the behavioral description. To support the top-down and modular development of a real-time specification in GCSR, we have augmented ACSR and thus GCSR with a refinement theory. The refinement theory allows relabeling of events, addition of implementation events, and substitution of a time and resource-consuming action with a process that may use fewer or more resources than the refined action. Consistency between an abstract specification and a refined specification is defined in terms of an ordering relation over traces that is extended to sets of traces according to the Hoare ordering or Egli-Milner ordering. The trace ordering relation relates traces that share timing properties such as equal duration and preservation of timed occurrences of communication events of the abstract specification. To facilitate the practical use of the refinement theory, we have characterized the extended trace ordering relations by a set of transformation rules that syntactically derive a refined process from an abstract one. The transformation rules define basic graphical operations that represent GCSR refinements. To experiment with the GCSR language and its refinement theory, we have developed a tool set that allows the specification, refinement, and analysis of real-time systems modeled in GCSR. We report our evaluation in the case of the Production Cell case study [LL95]