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

计算机工程与科学

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

胡启敏1,2,薛锦云 1,2 ,游珍1,2,程着1,2

(1.江西师范大学国家网络化支撑软件国际科技合作基地，江西南昌 330022;

2.江西省高性能计算技术重点实验室，江西南昌 330022)

收稿日期:2017-08-03 修回日期:2017-10-06 出版日期:2018-02-25 发布日期:2018-02-25
基金资助:
国家自然科学基金（61462041,61472167,61662036）;江西省自然科学基金（20171BAB202008）;江西省教育厅科技项目（160329）

Formal verification of serveral

software components in PAR platform

HU Qi-min1,2,XUE Jin-yun1,2,YOU Zhen1,2 ,CHENG Zhuo1,2

(1.Networked Supporting Software International S&T Cooperation Base of China,Jiangxi Normal University,Nanchang 330022;

2.Jiangxi Province Key Laboratory of High Performance Computing Technology,Nanchang 330022,China)

Received:2017-08-03 Revised:2017-10-06 Online:2018-02-25 Published:2018-02-25

摘要/Abstract

摘要：

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

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

Abstract:

PAR platform is a software platform developed by our research team to support software formality and automated development. The platform fully embodies the advantages of functional abstraction and data abstraction, thus making software development convenient and reliable. The key to achieving this performance is a batch of reusable software components. In order to ensure the correctness and reliability of the whole software platform, it is very important to ensure the correctness and reliability of the software components. In this paper, we select some typical software components in the PAR platform, formalize the semantics of the components in a formal way, and prove the correctness of the components with the help of the Coq theorem prover, hence improving the efficiency of software compoents’ formal verification.

Key words: software components, formal semantic, theorem proving, PAR platform, loop invariant

胡启敏1,2,薛锦云 1,2,游珍1,2,程着1,2. PAR平台中若干软件构件形式化验证技术研究[J]. 计算机工程与科学.

HU Qi-min1,2,XUE Jin-yun1,2,YOU Zhen1,2,CHENG Zhuo1,2.

Formal verification of serveral

software components in PAR platform

[J]. Computer Engineering & Science.

[1]	林玲瑜, 曹锋, 易见兵, 方旺盛, 李俊, 吴贯锋. 基于子句活跃度和复杂度的多元动态演绎算法及应用[J]. 计算机工程与科学, 2023, 45(12): 2256-2264.
[2]	刘永梅, 王国辉, 关永, 张景芝, 施智平, 董璐. 格林定理的形式化及其初步应用[J]. 计算机工程与科学, 2023, 45(07): 1178-1187.
[3]	张旭初, 石海鹤. 多序列比对算法族的形式化设计与生成[J]. 计算机工程与科学, 2020, 42(08): 1383-1392.
[4]	周哲泓1,2,3，薛锦云1,3，黄捷文1,2,3. 虚拟现实软件系统开发方法研究[J]. 计算机工程与科学, 2019, 41(11): 1968-1975.
[5]	章玥1,2，郭建1,2，朱晓冉1，王文君1，朱晶洋1，汤家华3，陈峻念3. 基于Event-B 方法的多应用智能卡的建模与开发[J]. J4, 2014, 36(10): 1943-1951.
[6]	陈石坤1，李舟军2. 基于QBF的循环不变式构造技术[J]. J4, 2010, 32(9): 76-80.
[7]	万松松1，2,薛锦云1，3,谢武平1. 循环不变式开发技术研究[J]. J4, 2010, 32(9): 84-88.
[8]	左正康, 游珍, 薛锦云. 后序遍历二叉树非递归算法的推导及形式化证明[J]. J4, 2010, 32(3): 119-123.
[9]	缪俞蓉程向红. 软件测试与软件设计方法分析[J]. J4, 2008, 30(4): 84-85.
[10]	王金双张兴元杨华兵张毓森. 并发系统概率空间的形式化构造方法[J]. J4, 2008, 30(11): 83-85.
[11]	石双元吴新明刘琦. 构件化信息系统体系结构及其业务构件模型研究[J]. J4, 2005, 27(5): 91-93.
[12]	李昌宇樊东平刘又诚. 以构架为中心的应用软件构件化开发方法[J]. J4, 2004, 26(1): 73-76.
[13]	胡峰林子禹等. 一种基于构件模型的分布式实时应用程序设计方法[J]. J4, 2003, 25(1): 10-12.