.png){kind=icon}
返回
End-to-End Formal Methods Integrated Development with SysMLv2 Using HAMR
.png){kind=icon}
PRE
AI
DOI：10.1007/978-3-032-00942-5_13.png)
.png){kind=icon}
原文求助.png){kind=icon}
分享.png){kind=icon}
收藏
摘要
En 中文
SAE标准化的AADL建模语言已成为学术界和工业界基于模型开发与集成形式化方法研究的重要推动力。然而，包括工业界偏好其他建模语言（如SysML）在内的多种因素，阻碍了AADL及其相关形式化方法技术的采用。对象管理组织（OMG）目前正在开发下一代SysML（SysMLv2），该版本吸纳了AADL的若干吸引人特性，并已授权实时嵌入式安全关键（RTESC）工作组考虑如何将AADL的概念、语义和形式化规范引入SysMLv2生态系统。本文报告了我们为HAMR形式化方法集成模型开发框架开发的SysMLv2前端。我们首次展示了如何利用RTESC SysMLv2库中的AADL概念，在多层次集成形式化方法的端到端代码生成工具中使用。我们描述了如何将GUMBO形式化组件契约语言集成到SysMLv2 AADL配置文件中，以提供：(a)基于SMT的模型级集成检查，以及(b)组件应用对架构契约的自动化测试和验证。我们提出了一种工具架构，该架构支持HAMR代码生成，目标为形式化验证的seL4微内核，以及其他形式化方法工具在Collins Aerospace DARPA PROVERS INSPECTA项目背景下应用于SysMLv2模型。
Keyword:
SysMLv2
AADL
formal methods
model-based development
HAMR
期刊
F
IF:
0
论文数:
15
被引数:
0
机构
引用论文
.png){kind=icon}
Ocarina : An Environment for AADL Models Analysis and Automatic Code Generation for High Integrity ApplicationsOcarina：用于高完整性应用AADL模型分析和自动代码生成的环境
PREAI
分享收藏分享收藏分享收藏
查看更多内容