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

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

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.