A Comparative Analysis of Formal languages Based upon Various Parameters

A Comparative Analysis of Formal languages Based upon Various Parameters

Javeria Jabeen

MS(CS) Student,UIIT PMAS Arid Agriculture University Rawalpindi, Pakistan

Mateen Ahmed Abbasi MS(CS) Student,UIIT PMAS Arid Agriculture University Rawalpindi,

Pakistan

Nasir Mehmood Minhas Assistant Professor, UIIT PMAS Arid Agriculture University Rawalpindi, Pakistan

Abstract-Formal method is collection of mathematics notations addressing the requirement specification, analysis and verification at any stage of the system life-cycle. Formal method identifies bugs or error in early stage of development. At the end product is delivered as per user requirement. Due to this reason many critical control systems are developed using formal methods. Formal method play silver built role in the software industry. Model based languages are Z, B and VDM are popular formal specification languages and mostly used in the industry. In this paper we compare three formal specification languages Z, B and VDM based upon various factor. The factors use for comparison is specification style, writing specification structure, support for object orientation, tool support, cost and Quality, Concurrency, Code generation, industrial application and domain.

Keywords- Formal specification language; Schema

1. INTRODUCTION

   Software engineering main focus is to develop the quality product/system. It is only possible when specification of the system is complete, correct and consistent. Formal specification is better way of identifying specification errors and describing system specification in unambiguous way. Formal specification language expressed the specification in a language whose vocabulary syntax and semantic are properly defined. Formal specification language provides mathematical representation of the system. Using formal method bugs find early and cost and time phase decreases in verification and testing phase. Quality of the product improves using formal method[1].

   We present formal specification language its advantages and disadvantages in 2ndSection. In 3rd Section, Z, B and VDM are examinedon base of aspects such as specification style, writing specification structure, support for object orientation, tool support, cost and Quality, industrial application and domain. Discussion is described in section

   1. Conclusions are presented in Section 5.

2. FORMAL SPECIFICATION LANGUAGES

   Formal Technique is mathematical model which is used to specify hardware and software of the system, verify the specification of the system and characteristics of the system. Formal method is applied during the development phase because it ensures that system is complete, correct and

   consistent specification.Formal specification language provides mathematical representation of the system.

   A formal language is collection of syntax, semantics and its relations.Semantics use to define Universe of Object

   .objects help foe defining the system. Relation defines the rule that indicate which objects satisfy the system specification[2].

   Advantages and limitations:

   Formal specification languages have many advantages which are discuss below.

   • Specifications are correct, complete and consistent.

   • A formal method is automatic verification of specification.

   • Specifications are non-Ambiguous.

   • Quality of the product is improved.[2]

     Limitations of formal method:

   • Customer cant easily understand the specification.

   • Difficult to learns and use the formal method.

   • Lack of tools support available for formal method.[3]

3. COMPARISON

   In this section we do comparison of the Z, B and VDM on the basis of the different parameters.

   1. Specification Style

      There are many styles exists for writing specification. Model based languages are Z, B and VDM. Z language describes system abstractly and it is based on mathematics. Z notation is not executable. B language is the combination of Abstract machine notation (AMN) and process of obtaining implementation form abstract model by stepwise refinement. Machine is directly translated into code. Compared to the B, Z is higher level language. Z, B, VDM all languages use set theory and logics. Vienna Development Method comprises a specification language and an approach to refining specifications into code.

      Process-oriented:These are designed to describe concurrent networks of communicating components behaviors. All types of the language which belongs to this category describe system in term of process[4].

      Sequential-oriented: Sequential system describe their input output behavior using sequential oriented.

      Model-oriented: The languages which fall in this type always constructs model of the system. Operations of that system are identified by state change or events that affect the model [5].

      Property-oriented: The languages which fall in this category identify the property that is desired by system. All type of the specification language which belongs to this category always emphases on the data type rather than functions of the system [4][5].

      TABLE 1.Comparison on the basis of specification style

      Z	B	VDM
      Sequential	Model	Process
      oriented,	oriented	oriented and
      Property oriented		model oriented
      and model
      oriented

   2. Writing specification structure

      Z specification is structure using schema. It has two parts first signature part identifiers are define or static component and second part is predicate part which has dynamic components. In the signature part contain list of declares the variable and predicate part contains list of the predicate. B specification is structure using B machine. Machine element is shown in the table given below. [6] VDM specification structure is not fix. In VDM define sets, invariants functions, support constant values and some other. In VDM languages sets are finite because they contain only a finite number of elements. VDM language supports only two types of function first order and higher order. [7] Define keyword that used in writing specifications of B and VDM-SL template.

      Machine: Machine Clause contained of machine name. Every machine name is unique.

      Variables: Variables clause contained all variables name that is used in machine.

      Initialisation: Initialization clause contained all initial state of the system.

      Invariant: in this clause define all the statements that should be true throughout the execution of operation.

      State: permanent data that must be stored by the system and which can be accessed by means of operations.

      Operations: that the system should be able to can accessed data. In this clause describe the checking pre conditions and providing post conditions that is intended to perform.

      Function: It defines as according to some rule input value maps to an output value.

      In VDM-SL specification its not necessary every clause would appear in every specification.

      TABLE 2.Comparison on the basis of writing specification structure

      Z	B	VDM
      SchemaName	Machine SETS, VARIABLES, ONSTRAINT INITIALISATION INVARIANTS OPERATIONS	Type Values State End Function Operation
      Signature Part Predicate Part

      Examples

      A public sector organization wants to computerize the system that records details about the phone numbers of staff. It wants to add employee. Assume that NAME is a set of names, and PHONE is a set of phone numbers.

      Z Notation

      B notation: MACHINE

      PhoneBook SETS

      NAME; PHONE

      VARIABLES

      known; Telephones

      INVARIANT

      known NAME ^

      telephones NAME PHONE ^ known=dom telephone INITIALISATION

      known; telephones := ;;

      OPERATIONS

      AddName (name_in, number_in)

      PRE

      name_inknown & name: NAME & phone : PHONE THEN

      telephone:=telephone {name_in phone} end

      VDM Notation:

      PhoneBook :: known : set of NAME Telephone : map NAME to PHONE Where

      Inv-PhoneBook known = dom telephone AddName (name: NAME, phone: PHONE) extwr Known : set of NAME

      wr telephone: map NAME to PHONE Pre

      name known post

      known = known name

      telephone = telephone {name phone}

   3. Object oriented concept.

      Z notation has a feature it break large specifications into smaller components. In object-oriented approach system is distributed into objects each of which has its own set of operations. In this way Z specification support Object oriented concept hence make specifications more easy [9].OOVDM supports two types of modules and inheritance mechanism, which are class modules and type modules. In Class modules define objects having their internal states. Type modules are those modules which specify objects with no states. OOVDM inheritance mechanisms are incremental inheritance and subtyping inheritance[8].

      TABLE 3.Comparison on the basis of object oriented concept

      Z	B	VDM
      Support Object	Not support object	VDM++ support
      oriented concept	Oriented	Object-Oriented
      using Object Z		concept
      		OOVDM

   4. Tool Support

      Formal languages such as Z, B and VDM have different types of tool. These tools are available in market and they support syntax checking, type checking, editing, creating and many others. [10], [11]

      TABLE 4. Comparison on the basis of Tool Support

      Z	B	VDM
      Z/Eves Z-word tool	Atlier-B B-Toolkit ProB	VDM Tools Overture.

   5. Cost and Quality

      Using Formal languages like Z, B and VDM in specification and design phase of SDLC not only uncovered the faults but also improved the design and understanding of the system. In 2009 researchers conduct survey on the use of formal method in 62 industrial projects. Main objective of this survey is count the effect of cost, time and quality using formal method. In this survey take 62 industrial project which cover mostly formal methods. As a result quality improved 92% and reduction of cost and time was reported.

      [12] Using formal method more effort being needed in the requirements and design phase and less in the implementation and testing. Using formal method cost saves and quality improve because error finds early stage in development [13]. In regulatory, commercial and Exploratory Cluster describe 12 cases in which 9 casa improve quality and 1 case is neutral and 2 casa are not available.[14]

   6. Domain

      This parameter describe domain of the formal languages for example reactive system, control system etc. Real time object Z is the combination of functional part and filter part. Functional part describes class and its behavior this division is non-real time. Filter section include timing constraint that are obligate on state schema and class which is identified in functional part. RTOZ is not standard .Event B is the extension in B formal language. VDM++ which is extension of the VDM. It support object oriented concept and it is more suitable language for real time system. [15][16][17]

      TABLE 5.Comparison on the basis of Domain

      Z	B	VDM
      Real time system using RTOZ	Event B use in reactive and distributed system	VDM++ Real-Time systems, Control Systems

   7. Concurrency

      In Formal specification languages some languages support concurrency. Concurrency is the property that allows many computations run simultaneously and potentially interact with each others[18].

      TABLE 6.Compariosn on the basis of concurrency

      Z	B	VDM
      Not support Concurrency	Not support Concurrency	VDM++ support Concurrency

   8. Code Generation

      Some formal specification languages generate automatic code generation forma the requirement specification[19], [20].

      TABLE 7. Comparison on the basis of code generation

      Z	B	VDM
      Software requirement		Software requirement	Software requirement
      specification cannot be		specification	specification
      automatically		automatically	automatically
      converted into		converted into	converted into
      computer source code		computer source code	computer source code

   9. Industrial Applications

      In many industrial projects Z, B and VDM were used. Formal specification languages mostly use for verification of safety critical systems. Z used in Storm Surge Barrier Control System for formally specification of design and use in Mondex Smart Card[21],[22]. METEOR project has convinced Matra Transport International of the advantages of using this B formal method [23]. B method use for metro line14 in paris and Roissy Charles de Gaulle airport shuttle [24].VDM use in TradeOne System aim is decrease

      the operating costs in trading securities. FeliCa Networks Project also use VDM++which use to generate IC chip which is embedded in cellular phone[25].

      TABLE 8. Comparison on the basis of Industrial application

      Z	B	VDM
      Storm Surge Barrier Control System Mondex smart cards	METRO Roissy Charles de Gaulle airport shuttle in Paris.	TradeOne Project FeliCa Networks Project

   10. Language Popularity in Project and industry

   Formal specification languages Z, B and VDM popular now a days because these languages are used in specification, designs and verification of the system. Every languages has own characteristic which spate each language from each others. Many survey conducted for check the popularity of the formal specification languages. We take 56 projects and its specification languages. According to these project VDM is popular other two languages. We take those projects which is mention in these references[12][13][26][27].

   Fig.1.Comparison on the basis of Popularity of languages

4. DISCUSSION

   Formal specification languages Z,B and VDM are model based languages. These languages support some parameters which are discussed in the comparison section. On the basis of these parameters we draw this graph which how Vienna developmentmethod (VDM) language satisfy more parameters and it is the best language other two formal specification languages. Languages popularity alsoshows that VDM is more popular in the industry and projects.

   Fig. 2. Language and Satisfied Parameter

5. CONCLUSION

Z, B,VDM formal specification language based on mathematics and all are model based specification language. These languages are used to specifying user requirement in the mathematical form. B and VDM formal languages translate specification into code directly. Z and VDM language both support object oriented concept. Tool support is available for these languages. Many successful projects available which proof formal method is reliable approach for safety critical system. These projects also tell the quality of the system improve using formal method. Formal method used to identify bugs or error early phases and cost of the project is decrease in testing and verification phase. Industrial survey proves that formal specification methods improves quality and reduce the cost of the projects. Future work is that assign weight to these parameters and then compared the formal specification languages.

REFERENCES

1. I.Sommerville, Formal Specification, 2009.

2. R. Pressman, Software Engineering- APractitioners Approach, McGraw Hill, 5th edition, 2000.

3. S. Liu, and R. Adam, "Limitations of Formal Methodsand an Approach to Improvement", Second Asia-Pacific Software Engineering Conference, 1995, pp. 498.

4. Dr. A.K.Sharma, and M. Singh, Comparison of the Formal Specification Languages Based Upon Various Parameters, IOSR, JCE, 2013, pp. 37-39.

5. J. Hui, L. Dong, and X.Xiren, Using Formal Specification Language in Industrial Software Development, Intelligent Processing Systems, IEEE ,Beijing, 1997, pp. 1847-1851.[1]

6. C. Ponsard, and E.Dieul, From Requirements Models to Formal Specifications in B, CEUR-WS.org, 2006.

7. P. G. Larsen ,K. Lausdahl, N. Battle ,J. Fitzgerald, and S. Wolff VDM-10 Language Manual, 2013.

8. A.Laorakpong, and M. Saeki, Object-oriented formal specification development using VDM, Object Technologies for Advanced Software Lecture Notes in Computer Science, Springer, 1993, pp. 529-543.

9. A. Hall, Seven Myths of Formal Methods, Software, IEEE, 1990, pp. 11-19.

10. S. K. M, and S. Goel, Specifying Safety and Critical Real-Time Systems in Z, IEEE, ICCCT, 2010, pp. 596-602.

11. D. Jackson, Software Abstractions: Logic, Language, and Analysis revised edition, 2012.

12. J. Woodcock, P. G. Larsen, J. Bicarregui, and J. Fitzgerald,Formal Methods: Practice and Experience .ACM Computing Surveys, 2009, pp. 1-40.

13. P. A. Geer, Formal Methods In Practice: Analysis and Application of Formal Modeling to Information System, 2011.

14. D. Craigen, T. Ralston, and S. Gerhart, An International Survey of Industrial Applications of Formal Methods, 1993.

15. K. Periyasamy and V.S. Alagar, Extending Object-Z for Specifying Real-Time Systems, 1998.

16. R. Sammi,I. Rubab, and M. A. Qureshi, Formal Specification Languages for Real-Time Systems, IEEE, 2010.

17. J. R. Abrial, and S. Hallerstede, Refinement, decomposition, and instantiation of discrete models: Application to Event-B, ASM, 2007, pp. 1-28.

18. J. Fitzgerald, P. G. Larsen and S. Sahara VDMTools: advances in support for formal modeling in VDM, 2007.

19. D. Méry and N. K. Singh Automatic Code Generation from Event-B Models, ACM, 2011.

20. Overture Tool Box. Overture: Formal Modelling in VDM. http://www.overturetool.org/.

21. G. Rozenberg, and F. W. Vaandrager, Lectures on Embedded Systems, Springer Berlin Heidelberg, Lecture Notes in Computer Science, 1996.

22. J. Woodcock, S. Stepney, D. Cooper, J. Clark, and J. Jacob, The Certification of the Mondex Electronic Purse to ITSEC Level E6, Formal Aspects of Computing, 2008, pp. 519.

23. J. M. Wing, J. Woodcock, and J Davies jimWorld Congress on Formal Methods in the Development of Computing Systems, Springer Berlin Heidelberg, 1999.

24. H. Treharne, S. King, M. Henson, and S. Schneider, In ZB 2005: Formal Specification and Development in Z and B,Lecture Notes in Computer Science. Springer Berlin Heidelberg, 2005.

25. P. G. Larsen, and J. Fitzgerald, Recent Industrial Applications of VDM in Japan, Electronic Workshops in Computing, The British Computer Society, 2007.

26. N. K. Sing, Using Event-B for Critical Device Software Systems, Springer Science &Busines, 2013.

27. D. Craigen, T. Ralston, and S. Gerhart, An International Survey of Industrial Applications of Formal Methods, National Institute of Standards and Technology, Computer Systems Laboratory, 1993.