Skip to main content


Aligning the map requirements modelling with the b-method for formal software development


Abdul Babar and Vladimir Tosic



University of Western Ontario


We present a software development approach that aligns a requirements elicitation technique with a formal method of software specification abstraction. The goal/strategy modeling technique Map augmented with Jackson’s context diagrams (representing environment) is used to elicit requirements and the B-method is used to translate Map requirements into formal specifications. Comprehensive tool support allows the B-method to refine and implement the specification correctly. Our approach brings improvement to an approach that uses generic requirements for rigorous software development. The resulting specification model bridges the gap between software requirements and formal specifications and supports automatic refinement of strategic requirements into software code. To illustrate how our approach bridges this gap, we discuss the Point of Sale (PoS) requirements model of Seven Eleven Japan (SEJ).

BibTeX Entry

    publisher        = {IEEE-CS},
    isbn             = {0-7695-3057-5},
    author           = {Babar, Abdul and Tosic, Vladimir},
    month            = dec,
    editor           = {{Hirohisa Aman}},
    year             = {2007},
    title            = {Aligning the Map Requirements Modelling with the B-method for Formal Software Development},
    booktitle        = {Asia-Pacific Software Engineering Conference},
    pages            = {17--24},
    address          = {Nagoya, Japan}


Served by Apache on Linux on seL4.