Answer Happy

You need to propose the Z formal specification for all the scenarios below. Design the required static schemas and relevant dynamic schemas based on the system requirements. a) MySejahtera is a system developed for Kementerian Kesihatan Malaysia to fight the Covid-19 pandemic. One of the features is tracking people movement with the function to scan QR code of certain locations. Model Z specification for the checking function with these requirements. i. ii. iii. i. b) From the specifications produced in 1a), you need to do specification refinement by implementing an array to the abstract set with these requirements. Develop a refine schema which uses set arrays of hwm (high water mark) and represent the abstract set using the array set. Design a schema to combine the abstract and refine schema. Develop the refine schema for record of the check-in and add location using refined schema. Initialise the refined schema. ii. iii. Record the premises and visitors during the check in process and only registered premises can record the check in process. iv. Add the locations of premises, but each premise is unique, where known premises cannot be added. Initialise the specification with an empty set.