文献类型：期刊文章

作　　者：胡启敏[1,2] 薛锦云[1,2] 游珍[1,2] 程着[1,2]

机构地区：[1]江西师范大学国家网络化支撑软件国际科技合作基地,江西南昌330022 [2]江西省高性能计算技术重点实验室,江西南昌330022

出　　处：《计算机工程与科学》

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

年　　份：2018

卷　　号：40

期　　号：2

起止页码：268-274

语　　种：中文

收录情况：BDHX、BDHX2017、CSCD、CSCD_E2017_2018、INSPEC、JST、ZGKJHX、核心刊

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

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

分 类 号：TP311.5]