Subject :Formal Methods, Formal Methods in Software Engineering

Question 04: [Marks : 15] Formally specify the system in Z. Consider a system that registers patients at a doctor's surgery. Assume that the surgery can deal with a maximum of 200 patients on its register. It will be necessary to add and remove patients from the register. The register must be able to be interrogated so that the list of patients and the number of patients registered can be returned. The UML specification of the PatientRegister class is given below. PatientRegister reg : Patient [*] addPatient(Patient) remove Patient(Patient) getPatients() : [ * ] numberRegistered():Integer Define the state Schema and operational schema for Patient Register along with the constant that number of registered patients must not exceed the LIMIT