Information Technology Reference
In-Depth Information
Probably the closest to our tool is the automatic refiner tool created by Siemens/Matra
[7]. The tool automatically produces an implementable model in B0 language (a vari-
ant of implementable B) by applying the predefined rewrite rules. A large library of
such rules has been created specifically to handle the specifications of train systems.
The use of this proprietary tool resulted in significant growth of developer productivity.
Our work aims at creating a similar tool yet publicly available and domain-independent.
The idea of reuse via instantiation of generic Event B models has also been explored
by Silva and Butler [18]. However, they focus on the instantiation of the static part of
the model - the context - while our approach mainly manipulates its dynamic part.
Nevertheless, these two approaches are complementary and can be integrated.
Obviously the idea to use refinement patterns to facilitate the refinement process
was inspired by the famous collection of software design patterns [10]. However in
our approach the patterns are not just descriptions of the best engineering practice but
rather ”active” model transformers that allow a designer to refine the model by reusing
and instantiating the generic prefabricated solutions.
As a future work we are planning to further explore the theoretical aspects of the
proposed language of refinement patterns as well as extend the existing collection of
patterns. Obviously, this work will go hand-in-hand with the tool development. We
believe that by building a sufficiently large library of patterns and providing designers
with automatic tool supporting refinement process, we will facilitate better acceptance
of formal methods in practice.
Acknowledgements
This work is supported by IST FP7 DEPLOY project. We also would like to thank the
anonymous reviewers for their valuable comments.
References
1. RODIN Event-B Platform (2007),
http://rodin-b-sharp.sourceforge.net/
2. Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press,
Cambridge (2005)
3. Abrial, J.-R.: Extending B without Changing it. In: Proceedings of 1st Conference on the B
Method, Nantes, France, pp. 169-191. Springer, Heidelberg (1996)
4. Back, R., Sere, K.: Superposition refinement of reactive systems. Formal Aspects of Com-
puting 8(3), 1-23 (1996)
5. Back, R., von Wright, J.: Refinement Calculus: A Systematic Introduction. Springer,
Heidelberg (1998)
6. Back, R.-J., Sere, K.: Stepwise Refinement of Action Systems. In: Proceedings of the In-
ternational Conference on Mathematics of Program Construction, 375th Anniversary of the
Groningen University, London, UK, pp. 115-138. Springer, Heidelberg (1989)
7. Burdy, L., Meynadier, J.-M.: Automatic Refinement. In: Workshop on Applying B in an
industrial context: Tools, Lessons and Techniques - Toulouse, FM 1999 (1999)
8. Butler, M., Grundy, J., Langbacka, T., Ruksenas, R., von Wright, J.: The Refinement Calcu-
lator: Proof Support for Program Refinement. In: Proc. of Formal Methods Pacific (1997)
9. Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)
