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

详细信息    查看全文 | 推荐本文 |

英文篇名：Formal verification of serveral software components in PAR platform 作者：胡启敏 ; 薛锦云 ; 游珍 ; 程着 英文作者：HU Qi-min;XUE Jin-yun;YOU Zhen;CHENG Zhuo;Networked Supporting Software International S&T Cooperation Base of China,Jiangxi Normal University;Jiangxi Province Key Laboratory of High Performance Computing Technology; 关键词：软件构件 ; 形式语义 ; 定理证明 ; PAR平台 ; 循环不变式 英文关键词：software components;;formal semantic;;theorem proving;;PAR platform;;loop invariant 中文刊名：JSJK 英文刊名：Computer Engineering & Science 机构：江西师范大学国家网络化支撑软件国际科技合作基地;江西省高性能计算技术重点实验室; 出版日期：2018-02-15 出版单位：计算机工程与科学 年：2018 期：v.40;No.278 基金：国家自然科学基金(61462041,61472167,61662036);; 江西省自然科学基金(20171BAB202008);; 江西省教育厅科技项目(160329) 语种：中文; 页：JSJK201802012 页数：7 CN：02 ISSN：43-1258/TP 分类号：82-88

摘要

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.

引文

[1]Xue J.A unified approach for developing efficient algorithmic programs[J].Journal of Computer Science and Technology,1997,12(4):314-329.
    [2]Xue J.Two new strategies for developing loop invariants and their applications[J].Journal of Computer Science and Technology,1993,8(2):147-154.
    [3]Xue Jin-yun.A practicable approach for formal development of algorithmic programs[C]∥Proc of the International Symposium on Future Software Technology,1999:158-160.
    [4]Xue Jin-yun.PAR method and its supporting platform[C]∥Proc of the 1st International Workshop on Asian Working Conference on Verified Software,2006:159-169.
    [5]Xue J,Davis R.A derivation and proof of Knuth’binary to decemal program[J].Software Concepts&Tools,1997,18(4):149-156.
    [6]Xue J,Davis R.A simple program whose derivation and proof is also[C]∥Proc of the 1st IEEE International Conference on Formal Engineering Method(ICFEM’97),1997:1.
    [7]Gries D,Xue Jin-yun.The hopcroft-tarjan planarity algorithm presentations and improvements:TR88-906[R].New York:Department of Computer Science,Cornell University,1998.
    [8]Xue Jin-yun,David G.Developing a linear algorithm for cubing a cycle permutation[J].Science of Computer Programming,1998,11:161-165.
    [9]The Coq proof assistant[EB/OL].[2014-01-01].http:∥coq.inria.fr/.
    [10]Bertot Y,Castéran P.Interactive theorem proving and program development-Coq’Art:The calculus of inductive constructions[M].London,UK:Springer,2004.
    [11]Nipkow T,Paulson L C,Wenzel M.Isabelle/HOL:A proof assistant for higher-order logic[M].London,UK:Springer,2002.
    [12]Lero X.Formal verification of a realistic compiler[J].Communications of the ACM,2009,52(7):107-115.
    [13]Boldo S,Jourdan J-H,Leroy X,et al.A formally verified C compiler supporting floating-point arithmetic[C]∥Proc of the 21st IEEE International Symposium on Computer Arithmetic,2013:107-115.
    [14]Evcik J,Vafeiadis V,Nardelli F Z,et al.Relaxed-memory concurrency and verified compilation[C]∥Proc of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages,2011:43-54.
    [15]Malecha G,Morrisett G,Shinnar A,et al.Toward a verified relational database management system[C]∥Proc of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages,2010:237-248.
    [16]Braibant T,Chlipala A.Formal verification of hardware synthesis[C]∥/Proc of the 25th International Conference on Computer Aided Verification,2013:213-228.