An Overview of Formal
Methods and future Perspective
Javed Iqbal: VU-ID: MS160400306
Science, Virtual University of Pakistan
Abstract—This document is a comprehensive
overview of formal method in simple and easy manner, so that one who want to
see the whole picture of formal method use this document. In this document Formal method brief introduction
and current work and it contribution to software industry and future
perspective is given. Formal method is used to formally define the 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
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.
Specification; Abstract Data; Formal; Hardware; Software; Requirement
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 budget. If error found at later stage
of development then it will effects the overall budget of software project.
If during 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.
The solution to the above problems
of software systems 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 languages.
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 is touched with conclusion and .
OF FORMAL METHODS
software development life cycle Formal methods can be used at many stages.
There are following achievements are given below:
1. 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 certain
methods make requirement specification complete in all respect that fully implements
the system at hand either hardware or software.
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.
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.
The Formal Specification Styles are specified as follows:
In 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.
Algebraic 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.
The process based formal specification
language is basically build 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).
of Formal Languages in SDLC
There are two places where
formal languages are used given below:
SRS (software requirement
specification) document describe the software system and it’s 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.
When 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
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.
b. Theorem Prover
Theorem proving is another approach for
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.
OF FORMAL METHODS
Although Formal methods has
significant place in software development process but there are some limitation
also which in turn create some problems. These are discussed below:
Correctness of requirement Specifications:
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 way 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
Correctness of Implementation:
task of identifying whether the program satisfies the written requirement. 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.
c. Correctness of Proofs:
of proofs play an 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 likewise execution.
are following reasons of failure of proof:
a) The program is wrong require some correction.
b) The program is correct, but there is way of
proofing it not found.
c) The program is correct, but there is no
OF FORMAL METHODS
The early exercises in the
production of software lifecycle i.e. requirements investigation and detail, is
the most essential. As indicated by one of the Standish Chaos report 9, half
of all task frustrations happen because of poor prerequisites detail. The best
utilization of formal techniques is at these beginning periods. It is strong to
compose a determination formally as opposed to composing a casual determination
and after that interpreting it. To distinguish irregularity furthermore, lack,
it is proficient to break down the formal determination as start of schedule as
possible 10. Along the benefits talked about above, there are different
advantages which are talked about as below:
Measure of correctness:
utilization of formal techniques gives a measure of the accuracy of a
framework, as restricted to the present procedure of quality measures.
Early defect detection:
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.
Guarantees of correctness:
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 path is difficult to
accomplish through testing.
specification detail compel the writer to find all types of queries that may be
leaved up to the coding. This lessens the mistakes that happen during or
subsequent to coding. Formal strategies have the property of fulfillment, i.e.
it covers all angles of the System.
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.
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.
Using the Template
After the text edit has been completed, the paper is ready
for the template. Duplicate the template file by using the Save As command, and
use the naming convention prescribed by your conference for the name of your
paper. In this newly created file, highlight all of the contents and import
your prepared text file. You are now ready to style your paper; use the scroll
down window on the left of the MS Word Formatting toolbar.
FUTURE OF FORMAL METHOD
FM (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
expected to scale up the documentations of formal techniques what’s more, the tool
support to make it simple to utilize.
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 of software industry may gain some knowledge in one place. Enormous
need in programming advancement is expected to make every one of the techniques
to be more particular for the requirement engineering stage since prerequisites
are essential building check on which the whole programming can be made-up. This
work inspire software engineers to work in formal methods to achieve quality of
system and security.
The template will number citations consecutively within
brackets 1. The sentence punctuation follows the bracket 2. Refer simply to
the reference number, as in 3—do not use “Ref. 3” or “reference 3” except
at the beginning of a sentence: “Reference 3 was the first …”
Number footnotes separately in superscripts. Place the
actual footnote at the bottom of the column in which it was cited. Do not put
footnotes in the reference list. Use letters for table footnotes.
Unless there are six authors or more give all authors’
names; do not use “et al.”. Papers that have not been published, even if they
have been submitted for publication, should be cited as “unpublished” 4.
Papers that have been accepted for publication should be cited as “in press”
5. Capitalize only the first word in a paper title, except for proper nouns
and element symbols.
For papers published in translation journals, please give
the English citation first, followed by the original foreign-language citation
Eason, B. Noble, and I.N. Sneddon, “On certain integrals of Lipschitz-Hankel
type involving products of Bessel functions,” Phil. Trans. Roy. Soc. London,
vol. A247, pp. 529-551, April 1955. (references)
Clerk Maxwell, A Treatise on Electricity and Magnetism, 3rd ed., vol. 2.
Oxford: Clarendon, 1892, pp.68-73.
Jacobs and C.P. Bean, “Fine particles, thin films and exchange anisotropy,” in
Magnetism, vol. III, G.T. Rado and H. Suhl, Eds. New York: Academic, 1963, pp.
Elissa, “Title of paper if known,” unpublished.
Nicole, “Title of paper with only first word capitalized,” J. Name Stand.
Abbrev., in press.
Yorozu, M. Hirano, K. Oka, and Y. Tagawa, “Electron spectroscopy studies on
magneto-optical media and plastic substrate interface,” IEEE Transl. J. Magn.
Japan, vol. 2, pp. 740-741, August 1987 Digests 9th Annual Conf. Magnetics
Japan, p. 301, 1982.
Young, The Technical Writer’s Handbook. Mill Valley, CA: University Science,