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

Formal verification of serveral software components in PAR platform

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

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

出　　处：《计算机工程与科学》2018年第2期268-274,共7页Computer Engineering & Science

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

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

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

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论]