PAR平台中若干软件构件形式化验证技术研究

• 作者: 游珍 程着 胡启敏 薛锦云
• 来源期刊: 计算机工程与科学
• 学科: 工学
• 关键词: 软件构件 形式语义 定理证明 PAR平台 循环不变式
• 年，卷（期）: 2018,（2）
• 所属期刊栏目: 软件工程
• 页码范围: 268-274
• 页数: 7页
• 分类号: TP311.5
• 字数: 6062字
• 语种: 中文
• DOI: 10.3969/j.issn.1007-130X.2018.02.011

摘要

PAR平台是本团队研制成功的支撑软件形式化和自动化开发的软件平台.该平台充分体现了功能抽象和数据抽象的优越性,使得软件开发变得便捷和可靠,达到这一性能的关键要素是一批可重用软件构件.为保证整个软件平台的正确性和可靠性,确保其中软件构件的正确性和可靠性就显得十分重要.选取PAR平台中若干典型软件构件,用形式化方法对构件的语义进行形式化描述,并借助Coq定理证明系统,对构件的正确性进行形式化验证,大幅度提高了软件构件形式化验证的效率.