Model to specify real time system using Z and Alloy languages: A comparative approach

Choice of a particular specification language depends on the type of product. Z and Alloy both are formal specification languages used for specifying the software requirements in a succinct manner. Alloy language is designed specifically for automatic analysis of any real time system. This paper proposes comparison between the effectiveness of Z and Alloy languages. An Automated Teller Machine (ATM) example has been considered as a case study for real time analysis and is used to demonstrate the comparative differences between the functionalities of Z and Alloy languages. To make the explanation more precise, we present formal specification of some states (wait or busy) and operations (withdrawal or balance enquiry) of ATM system using Z and Alloy languages. By using Z/EVES tool, the syntax of Z language is verified and instances of these states and operations are generated by using a tool Alloy Analyzer.