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.