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

Pnueli，Emerson，and SistlaCCR-0205571，CCR-0205483 and CCR-0205365“Towards a Seamless Process for the Development of Embedded Systems“嵌入式系统具有重要的经济意义，并且实际上正变得无处不在。它们已经成为涉及航空、军事、电信和过程控制应用的安全关键系统的组成部分。 由于人们期望嵌入式系统将成为许多普通消费电器的关键部件，因此对嵌入式系统的兴趣正在进一步增长。消费者将期望与最好品牌的汽车、电视机和冰箱相关的可靠性和可预测性水平。对于这些嵌入式应用程序来说，前几代消费者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.