Where academic tradition
meets the exciting future

You are here: TUCS > PUBLICATIONS > Publication Search > Deriving Formal Specifications...

Deriving Formal Specifications from Informal Requirements

Dubravka Ilic, Deriving Formal Specifications from Informal Requirements. In: 31st Annual International Computer Software and Applications Conference (COMPSAC 2007), 1, 145-152, IEEE Computer Society, 2007.

Abstract:

Ensuring dependability of software requires the use of formal methods. However, formal methods are still not widely accepted in engineering practice. One of the reasons for this is difficulty of deriving formal specifications from large and complex requirements given in natural language. In this paper, we propose an approach to deriving formal specifications of reactive systems starting from their requirements. We base our approach on proposing a new requirements language and show how to transform the informal requirements of a reactive system into requirements written in this language. The derived requirements allow us to better structure the informal requirements. We show how these requirements are then systematically translated into a formal specification in the B Method, which is our formal modelling framework. To validate the proposed approach, we conduct a case study and show how to obtain formal specification of a reactive routing protocol for ad-hoc networks – AODV (Ad hoc On-Demand Distant Vector) routing protocol.

BibTeX entry:

@INPROCEEDINGS{inpIlic07a,
  title = {Deriving Formal Specifications from Informal Requirements},
  booktitle = {31st Annual International Computer Software and Applications Conference (COMPSAC 2007)},
  author = {Ilic, Dubravka},
  volume = {1},
  publisher = {IEEE Computer Society},
  pages = {145-152},
  year = {2007},
}

Belongs to TUCS Research Unit(s): Distributed Systems Laboratory (DS Lab)

Edit publication