 Open Access
 Total Downloads : 2692
 Authors : Dr.(Mrs.) Arvinder Kaur, Ms.Samridhi Gulati, Ms. Sarita Singh
 Paper ID : IJERTV1IS4227
 Volume & Issue : Volume 01, Issue 04 (June 2012)
 Published (First Online): 01072012
 ISSN (Online) : 22780181
 Publisher Name : IJERT
 License: This work is licensed under a Creative Commons Attribution 4.0 International License
Analysis of Three Formal MethodsZ, B and VDM
Dr.(Mrs.) Arvinder Kaur Associate Professor, University School of Information & Communication Technology,
Guru Gobind Singh Indraprastha University, Dwarka, Sector16C, Delhi, India
Ms.Samridhi Gulati M.Tech. Student University School of
Information & Communication Technology,
Guru Gobind Singh Indraprastha University, Dwarka, Sector16C, Delhi, India
Ms. Sarita Singh M.Tech. Student University School of
Information & Communication Technology,
Guru Gobind Singh Indraprastha University, Dwarka, Sector16C, Delhi, India
Abstract
Formal methods provide a much needed solid software engineering foundation for the art of programming computers. Formal specifications can be used to provide an unambiguous and consistent supplement to natural language descriptions and can be rigorously validated and verified leading to the early detection of specification errors. Most of the software is delivered with some bugs, with lack of complete functionality and sometimes with cost overrun. Formal methods can be a silver bullet for software industry for solving these problems. This paper compares and contrasts the strengths and weaknesses of the model oriented formal specification languages such as Z, B and Vienna Development Method (VDM) basis of various factors.

Introduction
Formal methods are mathematically based techniques that can be applied throughout the development of a system to precisely describe a system and involve the use of refinement techniques and proof obligation at each stage to ensure the correctness, completeness and consistency of specification. The formal specification languages are based on set theory and first order predicate calculus, but this mathematical background was initially not fully formalized.[1]
In this paper we describe formal specification language and different formal specification styles in Section 2. In Section 3, Z, B and VDM are compared on the basis of factors such as characteristics, concurrency, object oriented concept, tool support, and code conversion. Conclusions are presented in Section 4.

Formal Specification Languages
This section describes an overview of formal specification languages.
The representation used in formal methods is called a formal specification language. The language is formal in the sense that it has a formal semantics and as a result can be used to express specifications in a clear and unambiguous manner. A formal specification language can be used to specify the task at hand in a clear and concise manner. As formal methods and formal specification language has sound mathematical basis, it provides the means of proving that specification is realizable, complete, consistent and unambiguous. Even the most complex systems can be modeled using relatively simple mathematical objects, such as sets, relations and functions [1].
A formal specification language is usually composed of three primary components or in mathematical term we can say that it consists of two sets syntax and semantics and a set of relation. [1]
The specific notation with which specification is represented is defined by syntactic domain or syntax. Formal techniques can have considerably different semantic domain. Semantics helps to define a universe of objects that will be used to describe the system. Set of relations defines the rules that indicate which objects properly satisfy the specification. Formal specification languages use mathematics as their basis. Most complex systems can be modelled using simple mathematical objects, such as sets, relations and
functions. A mathematical statement is unambiguous and precise, which provides a way to give convincing arguments to justify ones solutions, and allows proving that an implementation satisfies the mathematical specification [1].
Types of Formal Specification Styles

Model Based Languages
There are a number of different ways to write a precise specification. One approach is model based languages. In it the specification is expressed as a system state model. This state model is constructed using well understood mathematical entities such as sets, relations, sequences and functions. Operations of a system are specified by defining how they affect the state of the system model. Operations are also described by the predicates given in terms of pre and post conditions [2].
The most widely used notations for developing model based languages are Vienna Development Method (VDM) [4], Zed (Z) [3] and B [5].

Algebraic Specification
System behaviour is formally specified using a software engineering technique called, algebraic specification. These languages uses methods derived from abstract algebra or category theory to specify information systems. For the definition of abstract data types interface, algebraic approach was originally designed. Type operation is specified in order to define the type rather than the type representation. Ex LARCH, ASL, OBJ [6].

Process Oriented
Concurrent systems are described using process oriented formal specification language. A specific implicit model for concurrency is the basis for these languages. In these languages processes are denoted and built up by expressions and elementary expressions, respectively, which describe particularly simple processes by operations which combine processes to yield new potentially more complex processes. Ex Communicating Sequential Processes (CSP) [7].


Comparison between Z, B and VDM
Z notation is a formal specification language that works at a high level of abstraction so that even complex behavior can be described precisely and concisely and it was originally proposed by Jean Raymond Abrial in 1977 and was developed further at
the Programming Research Group at Oxford University [8], whereas the B formal method is the method of software development based on B, a toolsupported formal method based around an abstract machine notation, used in the development of computer software and was originally developed by JeanRaymond Abrial in France and the UK [9]. One of the longest established Formal Methods for the development of computerbased systems is termed as Vienna Development Method (VDM).It was originated at IBM's Vienna Laboratory [10] in the 1970s.The Z, B and VDM are model based languages, which usually model a system by representing its state as a collection of state variables, their values and some operations that can change its state. All are based on set theory and mathematical logic. VDM was used in programming language description and compiler design. The main goal was to develop the language's fundamental features and to establish some formal semantics. Z notation is a strongly typed [11] mathematical, specification language. It is not an executable notation; it cannot be interpreted or compiled into a running program. Compared to Z, B is slightly more low level and more focused on refinement to code rather than just formal specification hence it is easier to correctly implement a specification written in B than one in Z.

Characteristics
The following table distinguishes Z, B and VDM based on different characteristics [12], [13], [14]
Comparison Factor
Z
B
VDM
Formal
Method Style
Model
Oriented
–
Model
Oriented
–
odel –
Oriented
Mathematical Basis
Set Theory First order predicate Calculus
Set Theory First order predicate Calculus
Set Theory First order
predicate Calculus
Appearance Difference
Key Word oriented (eg, PRE, THEN , END, INVARIA
NT)
Boxes Schemas
or
Keyword oriented (e.g. pre
, post, invariant s)
Structuring
Abstract Machine Notation
Schema Calculus which allows
various schemas to
None
be combined to form new
schemas
Specification of State
Changes
None
Before: undecorate d variables After: primed variables
Identification of Inputs and Outputs
Input and output parameters are given
by an
operation header: Output<– Operation_ Name(Inpu
ts)
Inputs: variable names ending in ?
No explicit way of specifyin g

Before: hooked variables

After: unhooke d variables

Outputs: variable names ending in !
programming is an approach for developing software system based on the concepts of classes and objects. [15], [16]
Z
B
VDM
Support object oriented concepts such as
polymorphism, inheritance and encapsulation
Using Object
Z.
No support for object oriented concept
Support object oriented concepts such as
polymorphism, inheritance and encapsulation
Using VDM++.
Table 3. Comparison on the basis of Object Oriented
Concept
Table 1. Comparison on the basis of Characteristics


Concurrency
Concurrency is a property used in distributed system that enables software systems to be served in large scale distributed systems. This property allows several computations to execute simultaneously, and potentially interact with each other.
Z
B
VDM
No support for concurrency control
No support for concurrency control
Provide support for concurrency control using VDM++
Table 2. Comparison on the basis of Concurrency

Object Oriented Concept
The object oriented concepts such as inheritance, polymorphism, and encapsulation are supported by some formal specification languages. Object oriented

Tool Support
There are variety of robust commercially available tools that provide support for writing specification, proof obligation, refinement, syntax checking, type checking, editing, creating, proving theorems and many others. The table given below describes different types of tools and their features supported by Z, B and VDM. [17], [18], [19], [20], [21].
Z
B
VDM
Z Word Z/Eves
Fastest
AtlierB ProB
SpecBox Overture
VDM tools
Table 4. Comparison on the basis of Tool Support

Code Generation
Some formal specification languages support generation of computer source code from requirement specification.
Z
B
VDM
Software requirement specification cannot be automatically converted into computer source code.
Software requirement specification can be
automatically converted into computer source code.
Software requirement specification can be
automatically converted into computer source code.
Table 5. Comparison on the basis of Code Conversion


Conclusion
Though Z, B and VDM are model based formal specification languages used for specifying users requirements in a mathematical language that can be proved, verified and tested unambiguously. While the journey of all three languages starts at the requirements specification phase of the software development life cycle (SDLC) model, but their path divides after this phase. Z works on high level of abstraction of a system and provides a strong base for system designing and then testing it. However, B models the system in an abstract machine notation that can be used further to design system, generate its code and then refine and test the same. VDM was used to prove the equivalence of programming language concepts as part of compiler correctness arguments. While specification written using B and VDM can be used to generate computer source code directly, Z notation doesnt provide such functionality. Free tool support is available for all three languages. Z, B and VDM do not differ radically from one another. They are similar in their foundations and goals, and both allow the specifier to state requirements precisely and refine these specifications into designs correctly .Developing software with formal specification languages takes more time and hence money in comparison to the developing the same software without it but this access cost can be scarified in order to make software a reliable one and hence increase the trust of the customer in software industry.

REFERENCES

R. Pressman, Software Engineering A Practitioners Approach, McGraw Hill, 5th edition. 2000.

D. Bjorner. Pinnacles of software engineering: 25 years of formal methods. In Annals of Software Engineering, vol 10, 2000, pp. 1166.

J. Davies and J. Woodcock, Using Z: Specification, Refinement, and Proof, In Prentice Hall, 1996.

C. B. Jones, Systematic Software Development using VDM, In Prentice Hall, 1990.

S. Schneider, B Method An Introduction Palgrave, Cornerstones of Computing series, 2001.

J. Guttag and J. J. Horning, The algebraic specification of abstract abstract data types, Acta Inform., vol. 10, pp. 2752, 1978.

C. A. R. Hoare, Communicating Sequential Processes, In Prentice Hall, NJ., 1985.

J.R. Abrial, S. A. Schuman and B. Meyer: A Specification Language, in On the Construction of Programs,
Cambridge
University Press, eds. A. M. Macnaghten and R. M. McKeag, 1980 (describes early version of the language).

J.R. Abrial. The B Book – Assigning Programs to Meanings. Cambridge University Press, 1996.

D. Andrews. Report From The BSI Panel For The Standardisatio Of VDM (ist/5/50). In VDM '88 VDM  The Way Ahead. Springer Berlin/Heidelberg, 1988.

J.M. Spivey, The Z Notation,Reference Manual, 2nd edition, Prentice Hall International, 1992.

J. Davies and J. Woodcock, Using Z: Specification, Refinement, and Proof, In Prentice Hall, 1996.

C. B. Jones, Systematic Software Development using VDM, In Prentice Hall, 1990.

S. Schneider, B Method An Introduction Palgrave, Cornerstones of Computing series, 2001.

B. Mahony and J. S. Dong, Timed Communicating Object Z, In IEEE Transactions on Software Engineering, vol. 26, No. 2, February 2000.

Peter Gorm Larsen. VDM++ Tutorial At FM 06. Handout, 2006. http://fm06.mcmaster.ca/VDM++.

The BToolkit". BCore (UK) Limited. Archive.org.
2004. Retrieved February 22, 2012.

M. Saaltink, The Z/EVES System, in ZUM 97: The Z Formal Specication Notation, J. Bowen, M. Hinchey and D. Till, Eds., 1997, pp. 7285.

URL http://sourceforge.net/projects/zwordtools/.

Steria, AixenProvence, France. Atelier B, User and Reference Manuals, 1996.Available at http://www.atelierb.eu/index_en.html.

CSK SYSTEMS CORPORATION. VDMTools User Manual (VDM++) ver.1.2, 2008. http://www.vdmtools.jp/en/.
International Journal of Engineering Research & Technology (IJERT)
ISSN: 22780181
Vol. 1 Issue 4, June – 2012