版权所有 2018 卡内基梅隆大学。保留所有权利。本材料基于国防部根据合同编号 FA8702-15-D-0002 与卡内基梅隆大学合作资助和支持的工作,该合同旨在运营软件工程研究所,该研究所是联邦政府资助的研究和开发中心。本材料中的观点、意见和/或发现均为作者的观点、意见和/或发现,除非另有文件指定,否则不应被视为官方政府立场、政策或决定。无担保。本卡内基梅隆大学和软件工程研究所材料按“原样”提供。卡内基梅隆大学不对任何事项作任何明示或暗示的保证,包括但不限于对用途的适用性、适销性、排他性或使用该材料所获得的结果的保证。卡内基梅隆大学不对专利、商标或版权侵权作任何形式的保证。[分发声明 A] 本材料已获准公开发布和无限制分发。非美国政府使用和分发请参阅版权声明。本材料可以完整复制,无需修改,也可以书面或电子形式自由分发,无需正式许可。任何其他用途均需获得许可。许可请求应直接发送给软件引擎
版权所有 2019 卡内基梅隆大学。保留所有权利。本材料基于国防部根据合同编号 FA8702-15-D-0002 与卡内基梅隆大学合作资助和支持的工作,该合同旨在运营由联邦政府资助的研究和开发中心软件工程研究所。本材料中包含的观点、意见和/或发现均为作者的观点、意见和/或发现,除非另有文件指定,否则不应被视为官方政府立场、政策或决定。无担保。本卡内基梅隆大学和软件工程研究所材料按“原样”提供。卡内基梅隆大学不对任何事项做任何明示或暗示的保证,包括但不限于对适用性、适销性、排他性或使用该材料所获得的结果的保证。卡内基梅隆大学不对专利、商标或版权侵权做任何形式的保证。[分发声明 A] 本材料已获准公开发布和无限制分发。非美国政府使用和分发请参阅版权声明。本材料可以完整复制,无需修改,也可以书面或电子形式自由分发,无需正式许可。任何其他用途均需获得许可。许可请求应直接发送给软件引擎
13:00 - 15:00 演讲环节:安全与保障:AADL 主席:Andy Wallington 以 AADL 为中心的安全与保障演讲“使用 AADL 分析基于 ROS 的机器人应用程序;在原型工业机器人和软件上进行演示。”。Dominique Blouin“使用 Resolint 使 AADL 模型符合建模指南”。Isaac Amundson“FACE 和 AADL 模型之间的双向增量转换”。Dominique Blouin“使用 AADL 评估网络安全的架构属性”。Charles Payne
• 使用模块化开放系统方法 (MOSA) 和开放标准 (例如 FACE、HOST) 的开放系统架构 (OSA) – 减少开发进度和总生命周期成本 • 高效 (及时且经济高效) 的系统修改 • 集成/互操作性/适应性 – 竞争力 • 利用商业投资 • 超越/缓解技术过时 • 缓解供应商锁定风险 • 基于模型的工程 (MBE) – 基于模型的规范和获取 (使用 FACE 和 SysML) – 基于模型的分析 • 以架构为中心的虚拟集成过程 (ACVIP) – 缺陷和集成问题的早期分析检测 – 组合、增量和形式分析 – FACE 到 AADL 和 SysML 到 AADL 桥接
• 使用模块化开放系统方法 (MOSA) 和开放标准 (例如 FACE、HOST) 的开放系统架构 (OSA) – 减少开发进度和总生命周期成本 • 高效 (及时且经济高效) 的系统修改 • 集成/互操作性/适应性 – 竞争力 • 利用商业投资 • 超越/缓解技术过时 • 缓解供应商锁定风险 • 基于模型的工程 (MBE) – 基于模型的规范和获取 (使用 FACE 和 SysML) – 基于模型的分析 • 以架构为中心的虚拟集成过程 (ACVIP) – 缺陷和集成问题的早期分析检测 – 组合、增量和形式分析 – FACE 到 AADL 和 SysML 到 AADL 桥接
随着飞机系统变得越来越自主,人机角色分配发生变化,新的故障模式出现。这就需要一种方法来识别日益自主的系统 (IAS) 的安全要求,以及一个框架和技术来验证和确认 IAS 是否满足其安全要求。我们使用机组资源管理技术来识别安全人机协作行为的要求和行为。我们提供了一种方法来验证 IAS 是否满足其要求。我们将该方法应用于城市空中交通案例研究,其中包括两种应急场景:不可靠的传感器和中止着陆。对于此案例研究,我们用 Soar 语言实现了一个 IAS 代理,它充当所选应急场景的副驾驶并执行起飞和着陆准备,而飞行员保留最终决策权。我们用架构分析和设计语言 (AADL) 开发了一个正式的人机团队架构模型,并在 AADL 的假设保证推理环境 (AGREE) 附件中正式化了操作员和 IAS 要求。我们根据 IAS 和操作员的要求正式验证了人机团队的安全要求。我们开发了一个从 Soar 到 nuXmv 模型检查语言的自动翻译器,并使用 nuXmv 正式验证了 IAS 代理是否满足其要求。我们分享了在此过程中发现的设计和要求错误以及我们学到的经验教训。
基于模型的系统工程 (MBSE) 是一种采用的建模和开发方法,用于对复杂软件系统(如空间应用)进行正确的构建。TASTE [1] 是 ESA 支持的实用且成熟的 MBSE 工具集,可实现软件系统开发大部分阶段的自动化:(i) 通过多种建模和编程语言(例如 ASN.1、AADL、SDL、C/C++)进行异构系统设计,(ii) 代码生成、构建和部署二进制应用程序,(iii) 通过静态分析和模拟进行验证,以及 (iv) 通过模型检查对属性进行形式化验证。形式化验证功能最近已添加到 ESA 项目“空间系统形式化验证的模型检查”(MoC4Space) 中的 TASTE 工具集中,并在两个实际案例研究中进行了验证。在本文中,我们报告了项目期间的成果和经验教训。
网络物理系统 (CPS) 的工程需要大量专业知识来捕获系统需求并得出正确的解决方案。基于模型的工程和 DevOps 旨在高效地交付质量更高的软件。基于模型的工程依靠模型作为一流的工件来分析、模拟并最终生成系统的各个部分。DevOps 专注于软件工程活动,从早期开发到集成,然后通过在运行时监控系统进行改进。我们声称这些可以有效地结合起来,以改进 CPS 的工程流程。在本文中,我们介绍了 TwinOps,这是一种将基于模型的工程、数字孪生和 DevOps 实践统一在统一工作流程中的流程。TwinOps 说明了如何利用 MBE 和 DevOps 中的几种最佳实践来设计网络物理系统。我们使用数字孪生案例研究来说明我们的贡献,以说明 TwinOps 的优势,结合 AADL 和 Modelica 模型以及物联网平台。
国防部于 2018 年发布的数字工程 (DE) 战略以及 DE 方法在机械和电气工程领域的成功应用推动了 DE 方法在其他产品开发工作流程(如系统和/或软件工程)中的应用。预期的好处是改善沟通和可追溯性,减少返工和风险。组织已经多次展示了 DE 方法的优势,通过使用基于模型的设计和分析方法,如有限元分析 (FEA) 或 SPICE(以集成电路为重点的仿真程序),在流程早期进行详细评估(即左移)。然而,其他领域,如用于网络物理系统 (CPS) 的嵌入式计算资源,尚未有效地展示如何将相关的 DE 方法纳入其开发工作流程。尽管 SysML 得到了广泛支持,特定工具(例如 MathWorks ®、ANSYS ® 和 Dassault 工具产品)和 Modelica 和 AADL 等标准也取得了重大进展,但 DE 对 CPS 工程的好处尚未得到广泛实现。在本文中,我们将探讨 CPS 开发人员为何迟迟不愿接受 DE,应如何定制 DE 方法以实现利益相关者的目标,以及如何衡量支持 DE 的工作流程的有效性。
摘要。目前,制造可靠的无人机(无人机)是科学和技术的一项重要任务,因为此类设备在数字经济和现代生活中有很多用例,所以我们需要确保它们的可靠性。在本文中,我们建议用低成本组件组装四轴飞行器以获得硬件原型,并使用现有的开源软件解决方案开发具有高可靠性要求的飞行控制器软件解决方案,该解决方案将满足航空电子软件标准。我们将结果用作教学课程“操作系统组件”和“软件验证”的模型。在研究中,我们分析了四轴飞行器及其飞行控制器的结构,并提出了一种自组装解决方案。我们将 Ardupilot 描述为无人机的开源软件、适当的 APM 控制器和 PID 控制方法。当今航空电子飞行控制器可靠软件的标准是实时分区操作系统,该系统能够以预期的速度响应来自设备的事件,并在隔离分区之间共享处理器时间和内存。此类操作系统的一个很好的例子是开源 POK(分区操作内核)。在其存储库中,它包含一个四轴飞行器系统的示例设计,使用 AADL 语言对其硬件和软件进行建模。我们将这种技术与模型驱动工程应用于在真实硬件上运行的演示系统,该系统包含一个以 PID 控制作为分区过程的飞行管理过程。使用分区操作系统将飞行系统软件的可靠性提升到了一个新的水平。为了提高控制逻辑的正确性,我们建议使用形式验证方法。我们还提供了使用演绎方法在代码级别以及使用微分动态逻辑在信息物理系统级别验证属性的示例,以证明稳定性。