Programming Research Group Technical Monograph PRG-103

Jun Ginbayashi

MSc thesis September 1992, 103 pages, ISBN 0-902928-81-3

A specification method for business processes is presented, in which not only the processes but also the database integrity constraints are specified in Z based on the structure of an Entity-Relationship data model. The formality of Z facilitates strict reasoning about the correctness of the processes with respect to the database integrity constraints.

In this method, as in VDM, one can proceed towards the correct specification of a process by checking a series of proof obligations. The precondition of a process is determined as one attempts to discharge the proof obligations.

During the specification activity computer support may be useful. The rquirements for, and a prototype of, a support tool are also presented. Such a tool might be integrated into existing CASE tools, such as the Information Engineering Facility.