@unpublished{deploy211,
       booktitle = {ABZ 2010},
          volume = {to be },
           title = {Starting B Specifications from Use Cases},
          author = {Aryldo G Russo Jr and Thiago de Sousa},
            year = {2010},
         journal = {Abstract State Machines (ASM), Alloy, B and Z Conference},
             url = {http://deploy-eprints.ecs.soton.ac.uk/211/},
        abstract = {The B method is gaining visibility in formal methods com- munity due to excellent support for refinement. However, the traceability between the requirements and the formal model is still an issue of this method. On the other hand, use cases have become the informal industry standard for mapping functional requirements, describing the system's behavior using natural language. In this paper we show how controlled use cases can be used as a guideline for starting B specifications. In other words, our approach presents how a transaction, which is defined as an atomic part of the use case scenario, can be mapped as a B operation, providing a practical way to establish traceability between functional re- quirements and formal models.}
}

<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>