Model to specify real time system using Z and alloy languages: A comparative approach
Model to specify real time system using Z and alloy languages: A comparative approach
- Author(s): A.K. Dwivedi and S.K. Rath
- DOI: 10.1049/ic.2012.0149
For access to this article, please select a purchase option:
Buy conference paper PDF
Buy Knowledge Pack
IET members benefit from discounts to all IET publications and free access to E&T Magazine. If you are an IET member, log in to your account and the discounts will automatically be applied.
International Conference on Software Engineering and Mobile Application Modelling and Development (ICSEMA 2012) — Recommend this title to your library
Thank you
Your recommendation has been sent to your librarian.
- Author(s): A.K. Dwivedi and S.K. Rath Source: International Conference on Software Engineering and Mobile Application Modelling and Development (ICSEMA 2012), 2012 page ()
- Conference: International Conference on Software Engineering and Mobile Application Modelling and Development (ICSEMA 2012)
- DOI: 10.1049/ic.2012.0149
- ISBN: 978-1-84919-736-6
- Location: Chennai, India
- Conference date: 19-21 Dec. 2012
- Format: PDF
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. (6 pages)
Inspec keywords: specification languages; automatic teller machines; real-time systems; software tools; formal specification
Subjects: Formal methods; Financial computing
Related content
content/conferences/10.1049/ic.2012.0149
pub_keyword,iet_inspecKeyword,pub_concept
6
6