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.
