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

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

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

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 are touched with

conclusion and references.

2.

ACHIEVMENT OF FORMAL

METHODS

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

software.

Ø

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

certain methods.

3.

Formal Specification Paradigms:

The Formal

Specification Paradigms are specified as follows:

Ø Algebraic Specification Paradigms

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

Ø Process Oriented Paradigms:

The

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:

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.

Application

of Formal Languages in SDLC

There

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.

b. 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:

i.

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.

ii.

Theorem Proving

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.

4.

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:

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

4.2. Implementation:

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.

4.3. Correctness

of Proofs:

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

likewise execution.

There are following reasons of failure of

proof:

a.

The

program is correct, but there is way of proofing it not found.

b.

The

program is correct, but there is no

correctness proof.

c.

The

program is written wrong and requiring some corrections.

5.

BENEFITS OF FORMAL METHODS

The

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:

i.

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.

ii. Measure of correctness:

The utilization of formal techniques gives a

measure of the accuracy of systems, as restricted to the present process of

quality measures.

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.

iv. 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 paths is difficult to accomplish through testing.

v.

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.

6.

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:

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.

Work

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

of SDLC.

It is expected to scale up the documentations

of formal techniques what’s more, the tool support to make it simple to

utilize.

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

References

1

Boehm B. W.: Software Engineering Economics. Prentice

Hall, 1981

2

International Journal of Information and Computation Technology.

3

ISSN 0974-2239 Volume 3, Number 11 (2013), pp. 1217-1224

4

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.

5

Amla, Nina and Paul Ammann. “Using Z Specifications in

Category Partition Testing” IEEE, 1992, pp. 3-10.

6

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

7

“Formal Verification: Essential

for Complex Designs.” Computer Design 37(6), June 1998

8

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

9

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.

10

F. Jahanian and A. Mok. “Modechart: a specification language

for real-time systems” IEEE Transactions on Software Engineering,

12(9):890-904

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,

Heidelberg

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.