INCAPS,a subsystem of XYZ system,is an INteractive Computer-Assisted Proving System, The primary targets to develop it range from proving temporal logic formal theorem to verifying XYZ/SE program's correctness whi...INCAPS,a subsystem of XYZ system,is an INteractive Computer-Assisted Proving System, The primary targets to develop it range from proving temporal logic formal theorem to verifying XYZ/SE program's correctness which are supported respectively by the mechanized logics—FOTL logic and Hoare-like proof system.This paper discusses five main topics concerning INCAPS system: the rules,implementation,tactics,forward proof and backward proof.It also gives several typical exam- pies for demonstration of INCAPS' working principle.The achievement to data is that we have now ac- complished successfully the verification of the hierarchical specification of AB protocol and the correctness of XYZ/SE program.展开更多
基金This project is supported by the National Natural Science Foundation of China.
文摘INCAPS,a subsystem of XYZ system,is an INteractive Computer-Assisted Proving System, The primary targets to develop it range from proving temporal logic formal theorem to verifying XYZ/SE program's correctness which are supported respectively by the mechanized logics—FOTL logic and Hoare-like proof system.This paper discusses five main topics concerning INCAPS system: the rules,implementation,tactics,forward proof and backward proof.It also gives several typical exam- pies for demonstration of INCAPS' working principle.The achievement to data is that we have now ac- complished successfully the verification of the hierarchical specification of AB protocol and the correctness of XYZ/SE program.
