GCSR: A Graphical Language With Algebraic Semantics for the Specification of Real-Time Systems

Graphical Communicating Shared Resources, GCSR, is a formal language for specifying real-time systems including their functional and resource requirements. A GCSR specification consists of a set of nodes that are connected with directed, labeled edges, which describe possible execution flows. Nodes represent instantaneous selection among execution flows, or time and resource consuming system activities. In addition, a node can represent a system subcomponent, which allows modular, hierarchical, thus scalable system specifications. Edges are labeled with instantaneous communication actions or time to describe the duration of activities in the source node. GCSR supports the explicit representation of resources and priorities to resolve resource contention. The semantics of GCSR is the Algebra of Communicating Shared Resources, a timed process algebra with operational semantics that makes GCSR specifications executable. Furthermore, the process algebra provides behavioral equivalence relations between GCSR specifications. These equivalence relations can be used to replace a GCSR specification with an equivalent specification inside another, and to minimize a GCSR specification in terms of the number of nodes and edges. The paper defines the GCSR language, describes GCSR specification reductions that preserve the specification behaviors, and illustrates GCSR with example design specifications