Iqbal: VU-ID: MS160400306
Computer Science, Virtual
University of Pakistan
This document is a comprehensive
overview of formal method in simple and easy manner, so that one who wants to
see the whole picture of formal method uses this document. In this document Formal method brief introduction
and current work and its contribution to software industry and future
perspective is given. Formal method is used to formally define any system
behavior either it software or hardware system. Formally mean where mathematics
is used to define something as we know mathematics is only the concrete tool
which has no ambiguity. Computer Science is going to be very big field in
future so, it need treatments like mathematics because mathematics have very
rigorous in its nature. In Software Engineering software development is the main
stream in computer science, so it need some formal kind of treatment or a methodological
treatment for software development usually for very crucial software systems
i.e. missile control, atomic system and x-ray control system. Such as in algebraic
specification in Formal method first defines some abstract data type and then
possible operations on the abstract data type. In this document step by step
approach is followed to understand the concept of Formal method. Related
technical stuff or material also is given to give some technical flavor to this
document. Now in this age an increasing need of computer systems to use of
rigorous formal process. Formal Methods comprise of mathematical model and
treat software requirements and designs of systems in very formal way. This
document gives a whole picture of formal methods in perspective of future of
formal methods. This document is made for computer science geeks to give the
sense of use of formal methods in software development, very important with
respect to the requirement engineering.
Keywords—Algebraic; Specification; Abstract Data; Formal; Hardware;
Software; Requirement Engineering
Formal method is
used to specify abstract data type. Abstract Data type is type of data
container which type is specified at time of using at dynamic run time of
software program. As we know computer science is going to be increasing day by
day in few years and influence the society in dramatic way. The use of software
in human life is on the increase and as result complex software programs are
developed on the large scale. That is why developing large and complex software
is tedious task and cumbersome process. If there is no way to specify the
software before its construction then there is great chances that program is
not constructed as desired and malfunctions. Now in this era of business
environment main goal of software project is to fulfill the requirement purpose
of client. However, there is a great competition between Software Companies to
build high quality software in short time with low cost. Software Industry deal
with big problem that is releasing software on time and with require quality on
decided budget. If problems are identified on early stage of development of
software it will not took costly to rectify them which in turn reduce the cost
of overall project budget. If error found at later stage of development then it
will effects the overall budget of software project.
testing of software products any error is reported in requirement engineering
phase then software engineer need to correct it in requirement and all other places
such as in design and in coding which is very cumbersome process. Then again
test the software products. To avoid such kind of situations if software
projects we need some ways or methods that will resolve these problems in
software products and gives us full proof of confidence as in mathematics which
in turn reduce the overall cost of software project and time bound.
Appropriate solution to the above problem of software systems is the
use of Formal methods. This is some kind of mathematical ways to specify the
software specification or requirement called Formal methods. In Formal methods
to represent the specification of software systems we use formal specification
Writing formal specifications and analyzing those specifications and
some others specification belongs to the system at hand comes in domain of
Formal methods. Formal methods are used in different stages of development
process in software project. Formal methods are now considered to be part of
standards because it involves mathematics, like in other engineering fields. This
document describes different aspects of formal methods especially in
requirement engineering phase of development process of software project systems
in the physical world. One thing very important about Formal Specification only
talks about what, not talk about why this actually done at implementation level. In this document formal
method achievements are discussed in section 2 and formal specification styles
and types of methods are explain in section 3. In section 4 of this document limitation
of formal methods are presented and in section 5 many benefits of formal
methods are given and in section 6 future of formal method are touched with
conclusion and references.
ACHIEVMENT OF FORMAL
In software development life cycle Formal methods can be
used at many stages. There are following achievements are given below:
Automatic Code Generation is
another key factor in formal specification. A typical programmer write 15 lines
of code on the average but automation can do better stuff like code generation.
Formal methods make requirement specification complete
in all respect that fully implements the system at hand either hardware or
These Formal methods come when
we are going to design very critical systems which must provide reliability and
take less time and give us a sense of completeness. Formal Methods has proved
that security, bug free and right systems are only possible with the use of
formal techniques in software development.
Formal methods help to produce
specification that gives the actual client requirement in very formal way like
mathematics that looks different from simple requirement specification. This
type of specification has no ambiguity in it and easily verify with the help of
Formal Specification Paradigms:
Specification Paradigms are specified as follows:
Ø Algebraic Specification Paradigms
technique was initially designed for the defining of abstract data types and
interface. In algebraic specification we specify the system behaviour of
abstract data type using abstract algebra. There is famous family of language
for algebraic specification which LARCH and OBJ family of languages
Ø Process Oriented Paradigms:
process based formal specification language is basically building the specific
modal for concurrent systems. In these
languages processes are represented by expression and use the help of
elementary expression. In these languages processes are denoted by expressions
and are built up with the help of elementary expressions which intern yield
more complex process. There are many languages but the most popular is CSP
(Communicating Sequential Processes).
Ø Model Based Paradigms:
formal methods, model the system like mathematical object and apply
mathematical operation like we perform on set, and functions. In algebraic
specification system state is hidden but in VDM (Vienna Development Method), B
and Z (Zed specification) are two main modal based specification languages. Model
based languages are a way to write a specification. The operations on states
are defined in term of pre and post conditions and some invariant conditions.
of Formal Languages in SDLC
are two places where formal languages are used given below:
a. Requirement Gathering: (Specification)
SRS (software requirement specification)
document describe the software system and its characteristics which client
need. Formal languages describe the system and it function characteristics with
the internal detail also.
Z, VDM and Larch are utilized for specification
of sequential systems while other formal techniques, for example, CSP, CCS,
State diagrams, Temporal Logic, Lamport and I/O automata, concentrate on
indicating the conduct of concurrent systems. RAISE is utilized for dealing
with rich state spaces what’s more; LOTOS is one of the dialects for dealing
with complicated nature because of simultaneousness.
we write formal specifications we can check or verify it through formal Verification
which is the process to prove or disprove the completeness and correctness of
proposed system specification in mathematical way. There are two ways to verify
the given below:
In model checking, a finite state model of the
build and its state space is mechanically investigated.
Two well-known and equivalent model checkers are SPIN and NuSMV.
proving is another approach for verification of
a specification or checking the correctness of a
program. A model of the system is described in a
mathematical language and desired properties of the
model can be proven by a theorem prover. It is
mechanization of a logical
proof. The specification to
be checked by a theorem prover is written in a
mathematical notation. Z (pronounced ‘Zed’) is its well-known example.
LIMITATIONS OF FORMAL
Formal methods has significant place in software development process but there
are some limitation also which in turn create some problems. These are
In common situation client demands changes with
time and there is no way of catching all changing requirement in formal way of
specification. Hence there is no such a way that assure us how much complete
our specification are and correct at what extent. There are some ways although
in literature to handle this kind of problem of getting complete requirements
but at starting point we need to be informal to gather requirement. So there is
chance of missing some key requirement.
The task of identifying whether the program is
satisfies the written requirements or not with client requirements. To perform
this identification we can use Hoare
logic where we must find the invariant of loop or invariant condition which
is very crucial step and time taking. It is also not possible to give proof for
some programs which are not written with the view of correctness.
Rightness of proofs plays as a basic part in
formal techniques. Rightness proofs increase the probabilities that the program
is correct. It is generally hard to ensure about the rightness of detail and
There are following reasons of failure of
program is correct, but there is way of proofing it not found.
program is correct, but there is no
program is written wrong and requiring some corrections.
BENEFITS OF FORMAL METHODS
early exercises in the production of software lifecycle i.e. requirements
investigation and detail analysis, is the most essential. As indicated by one of
the Standish Chaos report half of all task frustrations happen because of poor
prerequisites detail. The best utilization of formal techniques is at these
beginning periods. To distinguish irregularity furthermore, it is proficient to
break down the formal specification as start of schedule as possible. Along the
benefits talked about above, there are different advantages which are talked
about as below:
Abstraction is the concept in software
engineering to cope with the problem of complexity by considering the only
related stuff of object under consideration and neglecting the all other stuff.
For small scale software code is written straight away, however this is not
true there are lots of programs with plenty of code, which not understandable
easily, we need some detailed information about the code to understand. We can
achieve complete picture of system by using Formal Specification of system.
ii. Measure of correctness:
The utilization of formal techniques gives a
measure of the accuracy of systems, as restricted to the present process of
iii. Early defect detection:
Formal Methods can be associated to the earliest
plan step in software production, with this earlier detection of error in
design can be caught more error at early stage of SDLC.
Formal investigation tools such as Model
checkers think about all possible paths of execution through the system. In the
event that there is any probability of an error/mistake, a model checker will
discover it. In a multithreaded framework where concurrency is an issue, formal
analysis can investigate all conceivable interleaving and occasion orderings.
This level of coverage of all paths is difficult to accomplish through testing.
The formality of the description
allows us to carry out rigorous analysis. Formal
descriptions are generally written from different points
of view, by which one can determine important
properties such as satisfaction of high level
requirements or correctness of a proposed design.
FUTURE OF FORMAL METHOD
Formal Methods is
an exceptionally dynamic research place with a wide range of strategies and
numerical models. In current situation, there isn’t available any one strategy
that satisfies all the security related requirements of building a safe formal
determination. Analysts and experts are persistently working around there and
subsequently picking up the advantages of utilizing formal techniques.
There so many future trends in formal method
of software Engineering but most probable are given below:
might be started to build up a formal technique that joins different advantages
of different techniques that core interest in building secure formal specification.
might be done to reduce the cost of utilizing formal strategies in various stages
It is expected to scale up the documentations
of formal techniques what’s more, the tool support to make it simple to
might be started on enhancing techniques and tools for discovering mistakes
with the goal that accuracy to the system is distinguished.
In this document,
I have tried to show diverse view of formal techniques. The significant
irregularities arise in programming / software projects because of poor requirement
Specification. Hence, formal methods are the only answer to this kind of issue
related to requirement engineering in SDLC and combining small specification to
make big and complex specifications. The research paper is arranged in manner
so that software engineer that want to start his career in software industry
may gain some knowledge in one place. Plenty of work in programming advancement
is expected to make every one of the techniques to be more specific for the requirement
engineering stage since prerequisites are essential building check on which the
whole programming can be made-up. This work inspires software engineers to work
in formal methods to achieve quality of system and security.
As in future
everything is going to be performed by computer or robotics using the
artificial intelligence which is also a very hot area of research and
development. Formal methods are the best way of achieving this kind of
automation, for this we need to do high productive work in this field and
require more future research in this field.
Formal Methods are going
to main stream in future of software development and other system development
i.e. hardware. Future is more tilted towards the automation and formal method
is very likely to be a path towards this tunnel.
Boehm B. W.: Software Engineering Economics. Prentice
International Journal of Information and Computation Technology.
ISSN 0974-2239 Volume 3, Number 11 (2013), pp. 1217-1224
D.H. Kitson and S. Masters, An
Analysis of SEI Software Process Assessment Results: 1987-1991, Software
Engineering Institute, CMU/SEI92-TR-24, July 1992.
Amla, Nina and Paul Ammann. “Using Z Specifications in
Category Partition Testing” IEEE, 1992, pp. 3-10.
“Specification and Description
Language (SDL-92).” Z.100 (3/93). “SDL Combined with ASN.1.” Z.105 (3/95). ITU
General Secretariat, Sales Section, Place de Nations, CH-1211 Geneva 20.
“Formal Verification: Essential
for Complex Designs.” Computer Design 37(6), June 1998
Mark A. Ardis, John A. Chaves, Lalita J. Jagadeesan, Peter Mataga,
Carlos Puchol, Mark G. Staskauskas, and James Von Olnhausen. “A Framework
for Evaluating Specification Methods for Reactive Systems: Experience
Report” IEEE Transactions on Software Engineering, Vol. 22, No. 6, June
1996, pp. 378-389
Nancy Day. “A Model Checker for Statecharts (Linking CASE
tools with Formal Methods)” Technical Report 93-35, Department of Computer
Science, University of British Columbia, October 1993.
F. Jahanian and A. Mok. “Modechart: a specification language
for real-time systems” IEEE Transactions on Software Engineering,
12 Wing J.M. (1998) Formal Methods: Past, Present,
and Future. In: Hsiang J., Ohori A. (eds) Advances in Computing Science ASIAN
98. ASIAN 1998. Lecture Notes in Computer Science, vol 1538. Springer, Berlin,
13 C. T. Chou, P. K. Mannava, S. Park, “A simple
method for parameterized verification of cache coherence protocols”, Formal
Methods in Computer-Aided Design, pp. 382–398, 2004.
14 Gaudel, M. -C. (1994). “Formal
specification techniques”. Proceedings of 16th International
Conference on Software Engineering. pp. 223–223
15 Cliff B. Jones (1986). Systematic Software
Development using VDM. Prentice Hall International. ISBN 0-13-880717-5.
16 LOTOSphere: Software Development with LOTOS,
Tommaso Bolognesi, Jeroen van de Lagemaat, and Chris Vissers, editors, Kluwer
Academic Publishers, 1995
17 Peter Gorm Larsen,
“Ten Years of Historical Development “Bootstrapping”
VDMTools”, In Journal of Universal Computer Science, volume 7(8), 2001
18 D. Dolle. Vital
software: Formal method and coded processor. In Proceedings of ERTS 2006, 2006.