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

摘要：

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

关键词：软件构件、形式语义、定理证明、PAR平台、循环不变式

所属期刊栏目：40

分类号：TP311.5(计算技术、计算机技术)

资助基金：国家自然科学基金61462041,61472167,61662036;江西省自然科学基金20171BAB202008;江西省教育厅科技项目160329

在线出版日期：2018-04-12（万方平台首次上网日期，不代表论文的发表时间）

页数：共7页

页码：268-274