DocumentCode :
3108227
Title :
Verifying the CICS File Control API with Z/Eves: An Experiment in the Verified Software Repository
Author :
Freitas, Leo ; Mokos, Konstantinos ; Woodcock, Jim
Author_Institution :
Univ. of York, York
fYear :
2007
fDate :
11-14 July 2007
Firstpage :
290
Lastpage :
298
Abstract :
Parts of the CICS transaction processing system were modelled formally in the 1980s in a collaborative project between IBM 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 on using the Z/Eves mechanical 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.
Keywords :
application program interfaces; file organisation; program verification; CICS file control API; CICS transaction processing system; Z/Eves mechanical theorem prover; machine-checked analysis; software repository; Automatic programming; Automation; Collaborative software; Computer science; Documentation; Formal specifications; Laboratories; Reliability theory; Smart cards; Software engineering;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Engineering Complex Computer Systems, 2007. 12th IEEE International Conference on
Conference_Location :
Auckland
Print_ISBN :
0-7695-2895-3
Type :
conf
DOI :
10.1109/ICECCS.2007.45
Filename :
4276325
Link To Document :
بازگشت