Innovative Programming Technology for Embedded Systems

点击翻译按钮获取中文摘要

Innovative Programming Technology for Embedded SystemsThis is a proposal to provide innovative programming technology fordesigning and implementing reliable distributed embedded systems. The proposaladdresses a critical generic problem and a major opportunity. The genericproblem is that the research community does not know how to scale logicalmethods that are known to improve programs and small systems to the task ofimproving larger systems. The opportunity is that new methods of factoring arepossible for embedded systems, and new kinds of specifications are important.This project approaches the problem/opportunity by creating advanced logicalmethods and tools to structure embedded systems in a new way and to draw onrelevant formal knowledge about them to accelerate both the design and codingprocess and to improve the quality of the system code and its documentation.The project will add extensive formal knowledge to a logical programmingenvironment (LPE) and use it to generate system components that are correct byconstruction and to combine components based on semantic methods. Thesemantics supports formal classes and aspect-oriented programming. One testcase for the new methods is a particular distributed embedded system calledMediaNet -- a system for processing various media (audio, video, text) over adistributed computing network to adaptively respond to quality of serviceconstraints.The project will use mathematical knowledge about media streams and transitionsystems to precisely formulate design requirements and component functionality.Quality of service constraints will be incrementally added to the functionalspecifications and used to automatically modify the proof and the extractedcode so that these requirements are met. This is a very high level example offormal aspect-oriented programming and proof reuse.The library of formal knowledge about the system will be organized as amathematical theory. That organization draws on concepts about streamtransformers, the distributed network of machines, quality of serviceproperties and communication services. An expressive logic will be used tostate properties of the system and keep track of logical dependencies amongsystem components.The project team has considerable experience working together building andsupporting distributed communications systems by specifying and verifyingcommunication protocols and optimizing them using formal methods.