ITR: COLLABORATIVE RESEARCH: Towards a Seamless Process for the Development of Embedded Systems

Pnueli、Emerson和Sista CCR-0205571、CCR-0205483和CCR-0205365“迈向嵌入式系统开发的无缝过程”嵌入式系统具有重要的经济意义，从字面上讲正在变得无处不在。它们已经成为涉及航空、军事、电信和过程控制应用的安全关键系统的不可或缺的组成部分。人们对嵌入式系统的兴趣进一步增长，因为人们预计它们将成为许多普通消费设备的关键组件。消费者将期待与最好的汽车、电视和冰箱品牌相关的可靠性和可预测性水平。前几代消费类PC软件产品出现的故障、崩溃和一般不稳定的行为对于这些嵌入式应用程序来说是不可接受的。因此，这些嵌入式软件系统满足高水平的正确性标准变得至关重要，远远高于今天的大型软件系统，后者通常是高度容易出错的。除了对功能正确性的新标准的要求外，嵌入式系统还提出了以前的验证和验证方法没有完全解决的额外挑战。这包括对时效性的充分保证，低或可控的功耗，以及低或可控的内存利用率。随着嵌入式系统的普及，以及需要保证嵌入式应用程序的可接受级别的功能和可靠性，行业需要一个有效和可靠的开发过程。由于市场的限制，这样的流程还应该支持快速的周转时间，并使同一产品的许多定制变体的设计变得容易。该项目正在为如下所述的嵌入式系统的无缝设计流程奠定基础。特别是，它正在开发：一种用于需求的正式可视语言，包括行为、时间和TPM约束；用于从需求规范语言自动合成可执行规范的方法；用于对照需求验证系统的中间和分布式表示的方法；用于规范的自动代码分发的方法，可能具有用户提供的一些体系结构约束；用于表示硬件/软件协同设计平台的模型，该模型允许对松散耦合和紧密耦合的组件进行建模以及关于它们的组合推理；用于从可执行规范自动生成体系结构优化代码的算法；使用监视器对生成的代码进行翻译验证和在系统上进行运行时验证的方法；分析器进程的设计，该进程分析机器代码，计算时间、功率和内存的结果数字，并将这些数字与其可执行规范来源反向关联，从而实现对这些需求的早期分析。该项目的影响是简化并显著加快新产品的嵌入式应用程序以及现有产品线的修订和定制的上市时间。另一个影响是将嵌入式软件的可靠性和可预测性级别升级到新的标准，与最好的消费产品品牌预期的标准兼容和可比。

Pnueli, Emerson, and SistlaCCR-0205571, CCR-0205483 and CCR-0205365"Towards a Seamless Process for the Development of Embedded Systems"Embedded systems are of vital economic importance and are literallybecoming ubiquitous. They have already become an integral component ofsafety critical systems involving aviation, military,telecommunications, and process control applications. Interest inembedded systems is growing further due to the expectation that theywill become a key component of many commonplace consumer appliances.Consumers will expect levels of reliability and predictabilityassociated with the very best brands of cars, televisions, andrefrigerators. Glitches, crashes, and general erratic behavior of thesort seen with prior generations of consumer PC software products willbe unacceptable for these embedded applications. It thus becomescrucial that these embedded software systems satisfy high levels ofcorrectness criteria, well above those of today's large softwaresystems, which are often highly error-prone.Besides the requirement of a new standard of functional correctness,embedded systems pose additional challenges which were not fullyaddressed by previous validation and verification approaches. Theseinclude adequate guarantees of timeliness, low or controlled powerconsumption, and low or controlled memory utilization. With thespread of embedded systems, and the need to guarantee an acceptablelevel of functionality and reliability of the applications they areembedded in, the industry needs an effective and reliable developmentprocess. Due to market constraints, such a process should also supporta fast turn-around time as well as enable the easy design of manycustomized variations of the same product.This project is developing the foundation for a seamless designprocess for embedded systems as described below. In particular, it isdeveloping: A formal visual language for requirements, including behavioral, temporal, and TPM constraints; A methodology for the automatic synthesis of an executable specification from the requirement specification language; A methodology for the verification of the intermediate and distributed representation of the systems against requirements; A methododology for automatic code-distribution of specifications, possibly with some architectural constraints provided by the user; A model for representing hardware/software co-design platforms that enables modeling of both loosely- and tightly-coupled components as well as compositional reasoning about them; Algorithms for automatically generating architecture-optimized code from executable specifications; Methods for translation validation of the generated code and run-time validation on the system using monitors; The Design of a profiler process which analyzes machine code, computes the resulting figures for time, power, and memory, and back-associate these figures with their executable specification sources, enabling early-stage analysis of these requirements.The impact of the project is to streamline and significantlyaccelerate the time to market of embedded applications of both newproducts and revisions and customizations of existing product lines.Another impact is to upgrade the level of dependability andpredictability of embedded software to new standards, compatible andcomparable to those expected from the best brands of consumerproducts.