The open archive for STFC research publications

Full Record Details

Persistent URL http://purl.org/net/epubs/work/35203
Record Status Checked
Record Id 35203
Title Implementing Dynamic Aggregations of Abstract Machines in the B Method
Abstract We previously defined an extension to the B method to be able to dynamically aggregate components. The proposed extension allowed one to build specifications which can create and delete instances of machines at run time, a feature often associated with object oriented languages and not directly supported in the B method. In this paper, we study the refinement of specifications written using this extension. We define a procedure that, given a valid implementation of an abstract machine M , systematically generates an implementation for a machine representing a dynamic aggregation of ``instances'' of M . Moreover, the generated implementation is guaranteed to be correct by construction. Following the approach initiated in our previous work, the refinement process is defined in a way that is fully compatible with the standard B method.
Organisation CCLRC , BITD
Keywords Engineering
Funding Information
Related Research Object(s):
Licence Information:
Language English (EN)
Type Details URI(s) Local file(s) Year
Paper In Conference Proceedings Lecture Notes in Computer Science Volume 3308 / 2004 . Is in proceedings of: Sixth International Conference on Formal Engineering Methods (ICFEM) (ICFEM), Seattle USA, 8-12 Nov 2004. doi:10.1007/b102837 ICFEM2004.ps 2004