CPS: Medium: The Ectokernel Approach: A Composition Paradigm for Building Evolvable Safety-critical Systems from Unsafe Components

CPS：中：外内核方法：从不安全组件构建可演化安全关键系统的组合范式

• 批准号: 1035736
• 负责人: Tarek Abdelzaher
• 金额: $ 90万
• 依托单位: University of Illinois at Urbana-Champaign
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2010
• 资助国家: 美国
• 起止时间: 2010-08-15 至 2014-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1035736&HistoricalAwards=false
• 关键词: CPS; Medium; Ectokernel; Approach; Composition

The objective of this research is to develop a new approach for composition of safety-critical cyber-physical systems from a small code base of verified components and a large code base of unverified commercial off-the-shelf components. The approach is novel in that it does not require generating the entire code base from formal languages, specifications, or models and does not require verification to be applied to all code. Instead, an explicit goal is to accommodate large amounts of legacy code that is typically too complex to verify. The project introduces a set of verified component wrappers around existing unverified code, such that specified global system properties hold. The intellectual merit of the project lies in its innovative approach for managing component interactions. Unexpected interactions are the primary source of failure in cyber-physical systems. A fundamental conceptual challenge is to understand the different interaction spaces of cyber-physical system components and determine a set of trigger conditions when certain interactions must be restricted to prevent failure. The project develops analysis techniques that help understand the different interaction types and provides component wrappers to restrict them when necessary.Broader impact lies in significantly reducing the design and composition effort for the next generation of safety-critical embedded systems. A variety of student projects are being offered to undergraduates and graduate students. The researchers especially encourage women and minorities to participate. Outreach activity, such as hosting K-12 students on school field/science days, further strengthen the educational component. Technology transfer to John Deere is expected.

本研究的目的是开发一种新的方法，从一个小的代码库的验证组件和一个大的代码库的未经验证的商业现成的组件组成的安全关键的网络物理系统。该方法是新颖的，因为它不需要从形式语言、规范或模型生成整个代码库，也不需要对所有代码进行验证。相反，一个明确的目标是容纳大量的遗留代码，这些代码通常太复杂而无法验证。该项目在现有的未经验证的代码周围引入了一组经过验证的组件包装器，以便保持指定的全局系统属性。该项目的智力价值在于其管理组件交互的创新方法。意外的交互是信息物理系统故障的主要来源。一个基本的概念性挑战是了解信息物理系统组件的不同交互空间，并确定一组触发条件时，必须限制某些交互，以防止故障。该项目开发的分析技术，有助于了解不同的交互类型，并提供组件包装器，以限制他们在必要时。更广泛的影响在于显着减少设计和组合工作的下一代安全关键嵌入式系统。各种各样的学生项目正在提供给本科生和研究生。研究人员特别鼓励妇女和少数民族参与。外联活动，如在学校实地/科学日接待K-12学生，进一步加强了教育部分。预计将技术转让给John Deere。