基于AADL的形式化验证系统的方法、装置、设备及存储介质

本发明提供了基于AADL的形式化验证系统的方法、装置、设备及存储介质，包括有以下步骤:S101：基于EMF技术，构建AADL模型和时间自动机的元模型；S102：基于AADL模型元素和时间自动机模型元素的对应关系，借助ATL转换引擎，实现AADL模型到时间自动机模型的转换；S103：基于模型检查技术，编写形式化性质规约，通过对时间自动机进行验证，进而确认AADL模型是否满足性质规约；填补了目前基于模型的软件开发领域缺乏可用的形式化验证工具的问题，可以实现自动化地验证基于AADL模型开发的软件系统的正确性，提高了软件产品的可靠性与安全性，降低了软件的测试成本；并且，还能够降低对使用者专业性的要求，提高了形式化性质规范的编写速度。