Innovative Programming Technology for Embedded Systems

嵌入式系统的创新编程技术这是一个为设计和实现可靠的分布式嵌入式系统提供创新编程技术的建议。 该提案涉及一个关键的一般性问题和一个重大机遇。 一般的问题是，研究界不知道如何扩展逻辑方法，已知的改善程序和小系统的任务，改善更大的系统。 机会在于，新的分解方法对于嵌入式系统是可能的，和新的规格是重要的。这个项目的方法的问题/通过创建先进的逻辑方法和工具，以新的方式构建嵌入式系统，并利用相关的正式知识来加速设计和编码过程，提高系统代码及其文档的质量，该项目将增加广泛的将形式化的知识转化为逻辑程序设计语言（LPE），并利用它生成结构正确的系统组件，以及基于语义方法的联合收割机组件的组合。 这些方法支持正式的类和面向方面的编程。 新方法的一个测试案例是一个特殊的分布式嵌入式系统MediaNet--一个处理各种媒体的系统（音频、视频、（正文）该项目将使用有关媒体流和传输系统的数学知识来精确地制定设计要求和组件功能。服务质量约束将逐步添加到功能规范，并用于自动修改证明和提取的代码，以便满足这些要求。 这是一个非常高层次的面向方面编程和证明重用的例子。关于系统的形式知识库将被组织为数学理论。 该组织借鉴了有关流变压器、分布式机器网络、服务质量特性和通信服务的概念。 一个表达逻辑将被用来陈述系统的属性，并跟踪系统组件之间的逻辑依赖关系。项目团队有相当丰富的经验，通过指定和验证通信协议，并使用形式化方法优化它们，共同构建和支持分布式通信系统。

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.