Verifying The Cics File Control Api With Z/eves: An Experiment In The Verified Software Repository

摘要

Parts of the CICS transaction processing system were modelled formally in the 1980s in a collaborative project between IBM UK Hursley Park and Oxford University Computing Laboratory. Z was used to capture a precise description of the behaviour of various modules as a means of communicating requirements and design intentions. These descriptions were not mechanically verified in any way: proof tools for Z were not considered mature, and no business case was made for effort in this area. We report a recent experiment in using the Z/Eves theorem prover to construct a machine-checked analysis of one of the CICS modules: the File Control API. This work was carried out as part of the international Grand Challenge in Verified Software, and our results are recorded in the Verified Software Repository. We give a brief description of the other modules, and propose them as challenge problems for the verification community.