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

摘要

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