A Case Study In Formal Specification

M. Sc. Thesis submitted to Sharif University of Technology - Computer Engineering Department

Author: Alireza Rouhi

Supervisor: Dr. Seyed- Hassan Mirian-Hosseinabadi

Internal examiner: Dr. Ali Movaghar

External examiner: Dr. Ayaz Isazadeh, E-mail: isazadeh@tabrizu.ac.ir

Defense Date: June 14, 2004

Abstract (Farsi)

Usage of Formal Methods, specifically in the specification phase, improves our understandings of the system requirements. As a result, produced system will be more consistent with the initial requirements. In this project, we experiment the usage of formal specification with the help of a case study. We select An Intelligent Registration Database System - which had been introduced and implemented by two ex-MSc students of Computer Engineering Department in Sharif University of Technology - as a case study, and extract the user requirements of the system. In the next step, we present the formal specification of the system in Z notation. We use the verification and proof tools to prove both the correctness of the specifications and the properties of the system. We report the results of these verficication activities and their effects on improving the specification. Finally, we apply the stepwise refinement method to generate codes from a part of the formal specifications of the system.

Keywords: Z Notation, Formal Specification, Verification, Refinement, Code Generation.

Last Updated:  February 01, 2008.