计算机工程与科学2018，Vol.40Issue(2)：268-274,7.DOI:10.3969/j.issn.1007-130X.2018.02.011
PAR平台中若干软件构件形式化验证技术研究
Formal verification of serveral software components in PAR platform
摘要
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.关键词
软件构件/形式语义/定理证明/PAR平台/循环不变式Key words
software components/formal semantic/theorem proving/PAR platform/loop invariant分类
信息技术与安全科学引用本文复制引用
胡启敏,薛锦云,游珍,程着..PAR平台中若干软件构件形式化验证技术研究[J].计算机工程与科学,2018,40(2):268-274,7.基金项目
国家自然科学基金(61462041,61472167,61662036) （61462041,61472167,61662036）
江西省自然科学基金(20171BAB202008) （20171BAB202008）
江西省教育厅科技项目(160329) （160329）
