Views in Z

Luke Wildman (2008). Views in Z PhD Thesis, The School of Information Technology and Electrical Engineering, The University of Queensland.

       
Attached Files (Some files may be inaccessible until you login with your UQ eSpace credentials)
Name Description MIMEType Size Downloads
s31715269_phd_correctedthesis.pdf s31715269_phd_correctedthesis application/pdf 1.51MB 8
Author Luke Wildman
Thesis Title Views in Z
School, Centre or Institute The School of Information Technology and Electrical Engineering
Institution The University of Queensland
Publication date 2008-08
Thesis type PhD Thesis
Supervisor Prof. Ian Hayes
Assoc. Prof. Roger Duke
Total pages 385
Total black and white pages 385
Subjects 08 Information and Computing Sciences
Abstract/Summary A specification of a software program, hardware component, or system, is a description of what the system is required to do without describing how it is to be done. Specifications provide the necessary details for system developers, suppliers, users and regulators to understand and agree upon the requirements of a system. It is therefore vital that specifications are clear, concise, complete, and are free of ambiguity and inconsistency. Specifications are usually expressed using a combination of informal natural language descriptions, diagrams, and formal mathematical techniques. The degree to which formal mathematics is used depends on the nature of the application and the criticality of the function being described. In industries where the cost of a system or software failure is high, such as national defence and government, banking, transport, energy, and communication, and some manufacturing industries, formal specification is recommended because it offers greater clarity and consistency, and moreover, formal specification are machine readable, allowing some automated checking to be applied. However, poorly written formal specifications can be less useful than informal specifications if they are unreadable (or not clear), or if they are overly large or complex (or not concise), making it hard to determine whether they are consistent or complete. In particular, if the system itself is large or complex, or it features multiple and diverse aspects of behaviour, it can be difficult to capture all aspects of its behaviour clearly and concisely in a monolithic formal model, or within a single formal notation. In many cases this is because the modeling approach may be particularly suited to some aspects of the system but not to others. The widely accepted solution to this problem is to use diverse modeling techniques to specify the different aspects of the system from different viewpoints. This results in a number of view specifications that taken together make up the complete specification of the system. The thesis introduces structuring mechanisms for the formal specification language Z that allow the view specifications of a system to be described, combined and reused. Specification encapsulation and parameter abstraction and application are explored along with object-oriented concepts such sub-typing and sub-classing. Two case studies, which are based on a language-based editor and a database system, are provided to illustrate how the techniques developed in this thesis may be used.
Keyword formal specification, views, viewpoints, requirements engineering, editors, databases

 
Citation counts: Google Scholar Search Google Scholar
Access Statistics: 54 Abstract Views, 11 File Downloads  -  Detailed Statistics
Created: Thu, 29 Oct 2009, 08:37:25 EST by Luke Wildman on behalf of Library - Information Access Service