%0 Journal Article %1 butler_08_incremental %A Butler, Michael %A Yadav, Divakar %D 2008 %J Formal Aspects of Computing %K 2008 b mondex \_pdf incremental \_to\_download event-b %N 1 %P 61--77 %R http://dx.doi.org/10.1007/s00165-007-0061-4 %T An incremental development of the Mondex system in Event-B %U http://dx.doi.org/10.1007/s00165-007-0061-4 %V 20 %X Abstract  A development of the Mondex system was undertaken using Event-B and its associated proof tools. An incremental approach was used whereby the refinement between the abstract specification of the system and its detailed design was verified through a series of refinements. The consequence of this incremental approach was that we achieved a very high degree of automatic proof. The essential features of our development are outlined. We also present some modelling and proof guidelines that we found helped us gain a deep understanding of the system and achieve the high degree of automatic proof.

@article{butler_08_incremental, abstract = {Abstract\ \ A development of the Mondex system was undertaken using Event-B and its associated proof tools. An incremental approach was used whereby the refinement between the abstract specification of the system and its detailed design was verified through a series of refinements. The consequence of this incremental approach was that we achieved a very high degree of automatic proof. The essential features of our development are outlined. We also present some modelling and proof guidelines that we found helped us gain a deep understanding of the system and achieve the high degree of automatic proof.}, added-at = {2009-03-10T04:32:55.000+0100}, author = {Butler, Michael and Yadav, Divakar}, biburl = {https://www.bibsonomy.org/bibtex/231858ec839e7e2465d379052370c6d23/leonardo}, citeulike-article-id = {3102585}, doi = {http://dx.doi.org/10.1007/s00165-007-0061-4}, interhash = {acd6d6f0a1df23c210da34a1c14707e2}, intrahash = {31858ec839e7e2465d379052370c6d23}, journal = {Formal Aspects of Computing}, keywords = {2008 b mondex \_pdf incremental \_to\_download event-b}, month = {January}, number = 1, pages = {61--77}, posted-at = {2008-08-08 22:28:49}, priority = {4}, timestamp = {2009-03-10T04:32:55.000+0100}, title = {An incremental development of the Mondex system in Event-B}, url = {http://dx.doi.org/10.1007/s00165-007-0061-4}, volume = 20, year = 2008 }