Formal methods used for design

Published: Last Edited:

This essay has been submitted by a student. This is not an example of the work written by our professional essay writers.

Formal Methods

1.1. Overview

Formal methods based on the mathematical notations used for designing, specification and verification of hardware and software system. These mathematical notations are derived from the area of discrete mathematics such as set theory, functions, relations and graph theory. Due to the mathematical basis, formal methods provide a complete, consistent and correct model of a systems. Formal method can be used in any stage of the system development and it can also be used for removing the ambiguity, inconsistency and incompleteness from systems. Formal method can remove the flaws in early system development otherwise it can be discovered in costly debugging and testing phases [1]. Correctness of a system implementation can be verified by using formal method in the verification phase [2].

Graphical notations or natural language is the basis of traditional approaches which are used to write the specification of a system. Huge vocabulary of natural language has multi meaning which makes the specifications highly ambiguous [3]. Traditional approaches have lack the ability to prove the absence of error in the specification. The inconsistency and errors are hidden due to the ambiguous specification, which can discover only during the implementations. On the other hand, formal specification based on mathematical notations has same interpretation throughout the world [4]. Syntax and semantics are well defined in the formal specification. Formal specification is consistent, concise and it can prove the properties of the system without implementation.

The requirements engineering is most important step in high quality software development process. The architectural structure of the complex software systems and their components require careful management. Every software system implicitly use a theorem that if some condition are satisfied or not to accomplish the requirement of a software system thus there is need of code verification. Code verification is the attempt to prove these theorems or find why this theorem failed to achieve the desired properties of a system. Therefore formal method can useful for representing requirements[5], architectural structure and code verification. There are several formal methods exists, the most common and well known formal mathematical models that describe the systems functionality as a specification are as follow:

* Z pronounced as "Zed"

* Vienna Development Method (VDM)

* Communicating Development Sequential Process (CSP)

* Formal Development Methodology (FDM)

* Larch

Formal methods can be used to specify the aspects of a system, it can be used for software safety and security of a system where formal method can prove that unsafe state will not be occur or can not break the security of a system thus it can justify the cost used for formal verification of a system. Formal methods can also include the graphical languages such as data flow diagram used for specifying the functions of a system.

Formal methods have also have many computer based tools like Z/EVES and VDM. These tools increase the use of formal methods in widespread areas and have different advantages like some tools convert a specification into executable prototype of a system and some of them can animate the specification. Therefore converting specification into code leads in the future where the software systems are developed without programmers. New emerging technologies are requires the knowledge of formal methods to completely understand and use them effectively. These technologies are

* Rapid prototyping

* Formal inspections

* Structured programming

* Object Oriented Design

Consequently formal methods can provide more precise specification, an ability to verify designs before implementing it, higher quality, productivity and better communication.

1.2. Formal Specification

Mathematical description of a system is known as formal specification. Traditional ways of specification for software systems uses the text and diagrams which are imprecise and ambiguous. Important information is hidden behind the specification and errors are discovered later on implementation phase that is more expensive and may or may not be solved. Formal specification has ability to overcome these issues. Formal specification is precisely and correctly describes the properties of a system. A formal specification is strongly based on mathematical notation [6]. These mathematical notations are based on predicate logic, set theory and graph theory. Most common formal notations are Z, VDM and Larch. Computer assisted tools are available for formal notations like Z/EVES.

1.3. Z Notations

Programming Research Group of Oxford University has been developed the Z in the late 1970's [7], which is modeled oriented approach based on first order predicate logic and set theory. Using the mathematics alone has problems like very large specifications can not readable and manageable. Therefore Z notation includes schema notation for structured specifications as well as the mathematical notations and also formal text to explain the mathematical description. Moreover it provides the precise specification of a system and describes only what a system does rather than how it does. Z is a well known formal method approach which uses schemas to describe static and dynamic behavior of a system as described in [8]. Where static behavior includes:

* All the states that system can occupy

* The invariant relationships from state to state are maintain

And the dynamic behavior includes:

* All possible relation

* Relationships between input and output

* Change of the state

The specification written in Z notations can support by tools to check the syntax and type errors.

A brief introduction of some important operators and structures of Z is given by using a simple case study of login system. It is a system which records the users and their passwords and able to check correct user can login to the system. It can also able to add, delete, and change user and their password.

1.3.1. Basic Type

One or more basic type can be introduced and their scope extends from the definition to the end of specification. Basic type has no structure and detail of implementation. The basic types can be defined in between the square brackets. As in the login system is required basic type of user and password where each username and password is recorded. The definition is written as [USER, PASSWORD].

1.3.2. Free Type

Free type introduced the set of distinct constants. As in the login system describe the Status set as free type having two distinct constant login_successfuly and access_denied, as written below.

Status ::€½€ login_successfuly ¼€ access_denied

1.3.3. Schemas

A boxed notation called 'schemas' is used for structuring the Z specifications. Any size of specification can be written in Z notations by using the schemas. These have two parts dividing by a vertical or horizontal line, the first part is declaration which is used to define the variables and second part is predicate which define the relationship between the values of the variables, this relationship is true for every state of the system and is maintained by every operation on it.

The state of the Login System is defined as LoginSystem schema which is composed of users and passwords. The set of users contain the user names and set of passwords contains the password of different users. The userpassword is total function which maps USER to PASSWORD. Below the horizontal line a number of invariants on the elements of the LoginSystem schema are specified. All the user in the domain of the total function userpassword is the subset of user and all the password in the range of the total function userpassword is the subset of the passwords.


®users:  USER

®passwords:  PASSWORD

®userpassword: USER ¦ PASSWORD


®dom userpassword º users

®ran userpassword º passwords


In this schema, the invariant allows the value of the variable users to be used in the relation userpassword, users is a component of the state LoginSystem. To describe an operation which add a new user and change the content of LoginSystem.



®user?: USER

®password?: PASSWORD


®user? ƒ¤ users

®userpassword' = userpassword' • »€¨user? Œ password?€©½


The declaration DLoginSystem alters us to the fact that the schema is describing a state change by introducing four variables users, passwords, users' and passwords'. The users and passwords are the observations of the state before the change, and users' and passwords' are observations of the state after the change. Each pair of variables is implicitly constrained to satisfy the invariant therefore it must hold both before and after the operation. The declaration of the two inputs to the operation by writing the input variable name and end in question marks as user? and password?. The part of the schema below the horizontal line firstly gives a pre-condition for the success of the operation that the user to be added must not already be a member of users to the LoginSystem, secondly gives the post-condition add this user? and password? as a maplet to the relation userpassword.

The second operation of this case study is to delete the user from the LoginSystem, and we describe it with a schema DeleteUser.

ƒˆŸDeleteUser ŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸ


®user?: USER

®password?: PASSWORD


®user? ¥ users

®password? ¥ passwords

®user? Œ password? ¥ userpassword

®userpassword' = userpassword' \ »€¨user? Œ password?€©½


Again the declaration DLoginSystem indicate that the schema is describing a state change. The pre-conditions for the success of the operation that the user to be deleted must a member of users, the given password belong to the passwords and the maplet of these must be in the relation userpassword. The post-condition delete this user? and password? as a maplet to the relation userpassword.

The third operation of this case study is to change the user name of the user from the LoginSystem, and we describe it with a schema ChangeUserName.



®user?: USER

®password?: PASSWORD

®changeuser?: USER


®user? ¥ users

®password? ¥ passwords

®user? Œ password? ¥ userpassword

®changeuser? ƒ¤ users

®userpassword' = »€¨user? Œ password?€©½ ± »€¨changeuser? Œ password?€©½


Here DLoginSystem also shows that the schema is describing a state change. The pre-conditions for the success of the operation that the user to be changed must a member of users, the given password belong to the passwords, the maplet of these must be in the relation userpassword and changeuser? must not a member of users . The post-condition updates the user name of this user? to the login system.

The fourth operation of this case study is to change the password of the user from the LoginSystem, and we describe it with a schema ChangePassword.

ƒˆŸChangePassword ŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸ


®user?: USER

®password?: PASSWORD

®newpassword?: PASSWORD


®user? ¥ users

®password? ¥ passwords

®user? Œ password? ¥ userpassword

®newpassword? ƒ¤ passwords

®userpassword' = »€¨user? Œ password?€©½ ± »€¨user? Œ newpassword?€©½


The DLoginSystem also indicate that the schema is describing a state change. The pre-conditions for the success of the operation that password of a user to be changed, user must be a member of users, the given password belong to the passwords, the maplet of these must be in the relation userpassword and newpassword? must not a member of passwords. The post-condition updates the password of this user? to the login system by using the override operator which is update the maplet in the userpassword.

In order to check the Status whether a user login to the system as login_successfuly or access_denied , we describe a schema with the name of Login.



®user?: USER

®password?: PASSWORD

®report!: Status


®user? ¥ users ¦ password? ¥ passwords ¦ user? Œ password? ¥ userpassword

®ƒž report! = login_successfuly

®user? ƒ¤ users ¶ password? ƒ¤ passwords ¶ user? Œ password? ƒ¤ userpassword

®ƒž report! = access_denied


This schema illustrates new notations, the declaration XLoginSystem indicates that this is an operation in which the state does not change the values of users' and passwords' of the observations after the operation are equal to their values users and passwords respectively. The other notation is the use of a name ending in an exclamation mark for an output. The Login operation takes a user name and password as input and yields the corresponding status as output. The pre-condition for the success of the operation is that user? is one of the element in set users, password? is one of the element in set passwords and a maplet of user? Πpassword? in the relation of userpassword implies as an output report! = login_successfuly to the login system and user? is not the element in set users, password? is not the element in set passwords or not a maplet of user? Πpassword? in the relation of userpassword implies as an output report! = access_denied to the login system.

To finish the specification, we must show what the system state is when this is started. This is the intial state of the system, and it is also specified by a schema InitialLoginSystem.

ƒˆŸInitialLoginSystem ŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸ



®users = €°

®passwords = €°

®userpassword = €°


This schema describes a LoginSystem in which the set of users, passwords and the function userpassword are empty.

We have described a mathematical model of both state of our LoginSystem and the operations performed on it. The system objects of LoginSystem were described in terms of mathematical data types such as sets and functions. The description of the state space included an invariant relationship between the variables and functions.

1.3.4. Axiomatic Definition

Global variables and functions can be declared as axiomatic definition, and optionally can specify the constraints on their values. The variable that goes for axiomatic definition previously can not be defined as global variables. The scope of axiomatic definition starts from the declaration where we define the axiomatic definition to the end of specification.

® Declaration


®€ Predicate

Where the declaration part introduce one or more global variables and predicate part can describe the constraints on the value of variable that declared in the declaration part.

1.3.5. Generic Schema

The generic schema can define the same structure for a variety of different types with one or more generic formal parameters.

ƒˆŸ[X1,...,Xn ]ŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸŸ





Generic schemas have the similar definition as the regular schemas, but only difference is that the formal generic parameters added in generic schemas. The name of generic schema name also not has appeared before in the specification, where Xi is the formal generic parameters which can assign to the identifiers in the declaration.


[1] J. M. Wing, "A Specifier's Introduction to Formal Methods," IEEE Computer, Vol.23, No.9, pp: 8-24, 1990.

[2] J. Seung-Ju, R. Jungwoo and L.Y. Chang, "Design of software security verification with formal method tools," International Journal of Computer and Network Security, volume 6 - 9B, September 2006.

[3] R.S. Pressman, "software Engineering A Practitioner's Approach," Fifth Edition,978-0072496680,McGraw-Hill,2001.

[4] J.P. Bowen and M.G Hinchey, "The Use of Industrial-Strength Formal Methods," Proceedings of 21st International Computer Software & Application Conference(COMPSAC'97),pp.332-337, August 1997.

[5] V. George and R. Vaughn, "Application of lightweight formal methods in requirement Engineering", The Journal of Defense Software Engineering, 2003.

[6] J.M. Spivey, "An introduction to Z and formal specifications," Software Engineering Journal Volume 4, Issue 1, Jan 1989 Page(s):40 - 50

[7] B. F. Potter, J. E. Sinclair, and D. Till. An Introduction to Formal Speci¬cation and Z. Prentice Hall International Series in Computer Science, 1991.

[8] J. M. Spivey, "The Z notation, A Reference Manual," Englewood Cliffs, NJ, Prentice-Hall, 1989.