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 学生，进一步加强了教育内容。预计将向约翰迪尔转让技术。