An Overview of Formal

Methods and future Perspective

Javed Iqbal: VU-ID: MS160400306

Computer

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.

Keywords—Algebraic;

Specification; Abstract Data; Formal; Hardware; Software; Requirement

Engineering

I. Introduction

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 .

A. ACHIEVMENT

OF FORMAL METHODS

In

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.

2. Formal

methods make requirement specification complete in all respect that fully implements

the system at hand either hardware or software.

3. 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.

4. 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.

B. Formal

Specification Styles:

The Formal Specification Styles are specified as follows:

1.

Model Based

Languages:

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.

2.

Algebraic

Specification

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.

3.

Process Oriented:

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).

.

II. Use

of Formal Languages in SDLC

There are two places where

formal languages are used given below:

1.

Requirement Gathering:(Specification)

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.

2.

Testing (Verification):

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

given below:

a. Model

Checking

In model checking, a finite state model of the

system is

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

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.

A. LIMITATIONS

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:

a.

Correctness of requirement Specifications:

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 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

requirement.

b.

Correctness of Implementation:

The

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:

Rightness

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.

There

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

correctness proof

BENEFITS

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:

a.

Measure of correctness:

The

utilization of formal techniques gives a measure of the accuracy of a

framework, as restricted to the present procedure of quality measures.

b.

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.

c.

Guarantees of correctness:

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 path is difficult to

accomplish through testing.

d.

Error Prone:

Formal

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.

e.

Abstraction:

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.

f.

Rigorous Analysis:

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.

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.

Fig. 1.

)

Acknowledgment (Heading

5)

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:

a. Work

might be started to build up a formal technique that joins different advantages

of different techniques that core interest in building secure formal specification.

b. Work

might be done to reduce the cost of utilizing formal strategies in various stages

of SDLC.

c.

It is

expected to scale up the documentations of formal techniques what’s more, the tool

support to make it simple to utilize.

d. Work

might be started on enhancing techniques and tools for discovering mistakes

with the goal that accuracy to the system is distinguished.

CONCLUSION

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.

References

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

6.

1

G.

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)

2

J.

Clerk Maxwell, A Treatise on Electricity and Magnetism, 3rd ed., vol. 2.

Oxford: Clarendon, 1892, pp.68-73.

3

I.S.

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.

271-350.

4

K.

Elissa, “Title of paper if known,” unpublished.

5

R.

Nicole, “Title of paper with only first word capitalized,” J. Name Stand.

Abbrev., in press.

6

Y.

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.

7

M.

Young, The Technical Writer’s Handbook. Mill Valley, CA: University Science,

1989.