Specifying Requirements and Designs for Real-Time Systems

目的是开发一种语言和方法，用于指定并发分布式实时系统的需求和设计，包括监视和控制的物理环境。提出了一种新的、完整的、可执行的符号，称为通信实时状态机（CRSM），作为基础。它们本质上是通过单向通道同步通信的状态机；此外，CRSM还提供了一组新颖的小工具，用于描述定时属性和访问实时。本研究由五个相关部分组成。首先是进一步定义和实现基本的CRSM模型。另一种是开发一种结构方案，允许机器及其部件组成更高层次的实体。第三种方法是设计一种方法，将基于状态的CRSM方法与面向对象的模型相结合。研究的第四部分是开发形式化的推理方法和工具，用于证明和测试关于规范的断言。最后，将在一些实际应用中进行规范实验。

The purpose is to develop a language and methodology for specifying the requirements and design of concurrent distributed real-time systems, including the monitored and controlled physical environment. A new, complete, and executable notation, called communicating real-time state machines (CRSM), is proposed as a basis. They are essentially state machines that communicate synchronously over one-directional channels; in addition, CRSM has a novel and small set of facilities for describing timing properties and for accessing real time. The research consists of five related parts. The first is to define further and implement the basic CRSM model. Another is to develop a structuring scheme that permits the composition of machines and their parts into higher level entities. A third is to design a methodology that combines the state-based CRSM approach with an object-oriented model. A fourth part of the research is to develop formal reasoning methods and tools, for proving and testing assertions about specifications. Lastly, specification experiments will be performed on some substantial applications.