目录
目录README.md

codegeneration

介绍

模型驱动开发方法逐渐应用于航空航天等领域的安全关键软件设计与实现中。体系结构分析设计语言( Architecture Analysis and Design Language,AADL) 是一种标准化的嵌入式软件体系结构描述语言,通过建模、验证以及代码自动 生成为安全关键软件的设计与实现提供完整支持。然而,工业界实际代码是运行在具有不同特性的目标平台上的,例如 不同的软硬件体系结构和编程接口,而现有AADL 代码生成研究主要是通过手工将自动生成的代码集成到平台当中,存在 工作繁琐且易出错的问题。本项目致力于实现基于AADL模型到ADA和C代码的生成,以及coq语言的语义一致性证明代码。

负责单位:

南京航空航天大学

感谢大家参与贡献!

关于

基于推理证明的模型和代码语义一致性验证工具,协助设计测试人员验证代码与模型的一致性。

670.0 KB
邀请码