Deriving Formal Specifications from Informal Requirements

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.