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

合作研究：CSR--EHS：反应式和嵌入式系统的基于属性的开发

• 批准号: 0720581
• 负责人: Amir Pnueli
• 金额: $ 15万
• 依托单位: New York University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2007
• 资助国家: 美国
• 起止时间: 2007-08-01 至 2009-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0720581&HistoricalAwards=false
• 关键词: Collaborative; Research; CSR; EHS; Property

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.

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