An Approach Of Program Proof For Safety-Critical Software

In the field of safety-critical embedded system, the analysis and verification software has becomea very important hotspot in the software engineering research. Engineering method and formal methodcan ensure the safety of software. Formal method uses mathematical model to guide softwaredevelopment process, and it is a way to improve people’s confidence for system safety. Theoremproving adapts the logic description language to the related reasoning system in formal methods.Compared with model checking, it has superiority of avoiding constraints in the state space and relatedinputs of proving process. For safety-critical embedded software, operation expression model is aneffective method of formal modeling in the present of theorem proving. In this paper, a category oftypical embedded software in safety-critical aspect is proved by operation expression, and it designsand implements a prototype tool. The main contents of this paper include four parts as follows:Firstly, for the safe subset of the C language, it analyses about data types、expression、processcontrol.It provides transformation rules from safe subset of the C language to operation expression andprocess for system supporting the C language design standard.Operation expression model ispreprocessed, and provides generated algorithm of model tree.Secondly, with features of the analysis tree’s structure and the semantic characteristics ofoperation expression, it provides the semantic predicate calculation rules and the relevant process,andconstructs the analysis tree with complete semantic predicate.It designs a safety verification frameworkfor the analysis tree based on semantic predicate.With the digestion principle and Coq theorem prover,it gives the design structure of verification execution engine to achieve the specification verification.Thirdly, for the software supporting the safe subset of the C language,the paper provides a methodof safety analysis and verification, and designs a prototype tool(OESPA).It introduces OESPAfunctional modules,and gives the design framework and bussiness processes.Finally, for SFCU case, it uses OESPA to verify safety-critical module with the requirement of thesystem and field standards.Meanwhile,it gives the relevant verification result and shows the feasibilityand effectiveness of this method.