Collaborative Research: CSR--EHS: Property-Based Development of Reactive and Embedded Systems

嵌入式系统在经济上具有至关重要的意义，而且实际上正在变得无处不在。它们已经成为涉及航空、军事、电信和过程控制应用的安全关键系统的不可或缺的组成部分。人们对嵌入式系统的兴趣正在进一步增长，因为人们期望它们将成为许多普通消费电子产品的关键组件。消费者将期待与最好的汽车、电视和冰箱品牌相关的可靠性和可预测性水平。对于这些嵌入式应用程序来说，前几代消费类PC软件产品出现的故障、崩溃和一般不稳定的行为将是不可接受的。因此，这些嵌入式软件系统满足高级别的正确性标准变得至关重要，远远高于今天的大型软件系统，后者通常非常容易出错。该项目将致力于研究和开发一种新的嵌入式系统系统开发方法，从系统要求的基于属性的高级别规范开始，以无缝和严格的方式进行运行代码。建议的设计流程的核心是利用强大的新的有效方法从行为(即时间)规范中自动合成运行代码。这项技术将在两个地方使用：第一，为了确定给定的基于属性的规范是否可实现。然后，选择的设计模块，其性能不是关键的，将通过自动综合生成。自动综合也可用于设计的较大部分的快速原型制作。考虑到这一总体计划，开展了以下主要研究活动：(1)开发用于指定需求的形式的基于属性的语言，包括行为、时间和结构约束；由用于分析大规格的一致性和可实现性的有效算法支持；开发用于从需求规格语言自动合成可执行规格的方法学，用于检查大规格的可实现性，以及自动构建设计的选定模块；以及(3)利用翻译验证技术，开发用于对照需求验证系统的中间表示的方法。最近，基于属性的开发方法被成功地应用于硬件设计的派生。鉴于这一成功，将其应用于嵌入式系统的系统建设是非常有前途的。这项研究追求规范语言的泛化，以包括实时元素和连续信号，并扩展综合方法以适应实时和混合系统。凭借这些能力，该项目有望为构建嵌入式系统实现系统的软/硬件协同设计。

Embedded systems are of vital economic importance and are literally becoming ubiquitous. They have already become an integral component of safety critical systems involving aviation, military, telecommunications, and process control applications. Interest in embedded systems is growing further due to the expectation that they will become a key component of many commonplace consumer appliances. Consumers will expect levels of reliability and predictability associated with the very best brands of cars, televisions, and refrigerators. Glitches, crashes, and general erratic behavior of the sort seen with prior generations of consumer PC software products will be unacceptable for these embedded applications. It thus becomes crucial that these embedded software systems satisfy high levels of correctness criteria, well above those of today's large software systems, which are often highly error-prone. This project will engage in research and development of a novel methodology for the systematic development of embedded systems, starting at a high-level property-based specification of system requirements and proceeding in a seamless and rigorous manner towards a running code. Central to the proposed design flow is the utilization of powerful new effective methods for the automatic synthesis of running code from behavioral (i.e., temporal) specifications. This technology will be used in two places: first, in order to determine whether a given property-based specification is realizable. Then, selected modules of the design, whose performance is not critical, will be generated by automatic synthesis. Automatic synthesis can also be used for rapid prototyping of larger portions of the design.In view of this master plan, the following main research activities are pursued:(1) development of a formal property-based language for specifying requirements, including behavioral, temporal, and structural constraints; supported by effective algorithms for the analysis of large specifications for consistency and realizability; development of a methodology for the automatic synthesis of an executable specification from the requirements specification language, to be used both for checking the realizability of large specifications, and the automatic construction of selected modules of the design; and (3) development of methods for the verification of the intermediate representations of the systems against requirements, using the techniques of translation validation. The property-based development approach has been recently applied successfully to the derivation of hardware designs. In view of this success, the application to the systematic construction of embedded systems is highly promising. This research pursues the generalization of the specification language to include real-time elements and continuous signals, and extends the synthesis approach to accommodate real-time and hybrid systems. With these capabilities, this project is expected to enable systematic co-design of software/hardware for the construction of embedded systems.