本发明公开了一种基于源代码的模型验证装置,所述装置包括：源代码获取模块,用于获取目标源代码；第一模型生成模块,用于根据AADL建模技术将所述目标源代码进行建模后生成AADL模型；第二模型生成模块,用于基于预设转换方式将所述AADL模型转换生成时间自动机模型；模型检查模块,用于利用预设模型检测器对所述时间自动机模型进行检查。因此,采用本申请实施例,可以提高验证效率。
科研之友
微信
新浪微博
Facebook
分享链接
