The integrated specification and analysis of functional, temporal, and resource requirements

The integrated specification and analysis of functional, temporal, and resource requirements

The Graphical Communicating Shared Resources, GCSR, is a specification language with a precise, operational semantics for the specification and analysis of real-time systems. GCSR allows a designer to integrate the functional and temporal requirements of a real-time system along with its run-time resource requirements. The integration is orthogonal in the sense that it produces system models that are easy to modify, e.g., to reflect different resource requirements, allocations and scheduling disciplines. In addition, it renders the verification of resource related requirements natural and straightforward. The formal semantics of GCSR allows the simulation of a system model and the thorough verification of system requirements through equivalence checking and state space exploration. This paper reviews GCSR and reports our experience with the production cell case study.

图形化通信共享资源（GCSR）是一种规范语言，具有精确的操作语义，用于实时系统的规范和分析。GCSR允许设计人员将实时系统的功能和时间要求与其运行时资源要求相结合。这种集成是正交的，也就是说它所产生的系统模型易于修改，例如，以反映不同的资源要求、分配和调度规则。此外，它使与资源相关要求的验证自然而直接。GCSR的形式语义允许对系统模型进行模拟，并通过等价性检查和状态空间探索对系统要求进行全面验证。本文回顾了GCSR，并报告了我们在生产单元案例研究中的经验。