Article

Reuse of specification patterns with the B method

Authors:

Sandrine Blazy,

Frédéric Gervais,

Régine LaleauAuthors Info & Claims

ZB'03: Proceedings of the 3rd international conference on Formal specification and development in Z and B

Pages 40 - 57

Published: 04 June 2003 Publication History

Abstract

This paper describes an approach for reusing specification patterns. Specification patterns are design patterns that are expressed in a formal specification language. Reusing a specification pattern means instantiating it or composing it with other specification patterns. Three levels of composition are defined: juxtaposition, composition with inter-patterns links and unification. This paper shows through examples how to define specification patterns in B, how to reuse them directly in B, and also how to reuse the proofs associated with specification patterns.

References

[1]

Blazy, S., Gervais, F., Laleau, R.: Un exemple de réutilisation de patterns de spécification avec la méthode B. Techn. rep. 395, CEDRIC Laboratory, Évry, France, 2002. Available at http://cedric.cnam.fr/PUBLIS/RC395.ps.gz

[2]

Clearsy: http://www.atelierb-societe.com

[3]

Eden, A., Hirshfeld, Y., Yehudai, A.: LePUS - a declarative pattern specification language. Techn. rep. 326/98, Department of Computer Science, Tel Aviv University, 1998.

[4]

Flores, A., Reynoso, L., Moore, R.: A formal model of object-oriented design and GoF design patterns. Techn. rep. 200, UNU/IIST, Macau, 2000. Available at http://www.iist.unu.edu/

[5]

Fowler, M.: Analysis patterns: reusable object models. Addison-Wesley, 1997.

Digital Library

[6]

Frappier, M., Laleau, R.: Proving Event Ordering Properties for Information Systems. Proc. ZB2003, LNCS, Springer-Verlag, Turku, Finland, June 4-6, 2003.

[7]

Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design patterns: elements of reusable object-oriented software. Addison-Wesley, 1995.

Digital Library

[8]

Gervais, F.: Réutilisation de composants de spécification en B. Master's thesis, DEA IIE(CNAM)-University of Évry-INT, Évry, France, July 2002. Available at http://cedric.cnam.fr/PUBLIS/RC394.ps.gz

[9]

Laleau, R., Mammar, A.: An overview of a method and its support tool for generating B specifications from UML notations. Proc. ASE: 15th IEEE Conference on Automated Software Engineering, IEEE Computer Society Press, Grenoble, France, September 2000.

Digital Library

[10]

Lano, K., Bicarregui, J., Goldsack, S.: Formalising Design Patterns. Proc. BCS-FACS Northern Formal Methods Workshop, Springer-Verlag, 1997, Ilkley, United Kingdom, September 3-4, 1996.

Digital Library

[11]

Lau, K., Ornaghi, M.: OOD frameworks in component-based software development in computational logic. Proc. LOPSTR'98, LNCS 1559, pages 101-123, Springer-Verlag, 1999, Manchester, United Kingdom, June 15-19, 1998.

Digital Library

[12]

Marcano, R., Meyer, E., Levy, N., Souquieres, J.: Utilisation de patterns dans la construction de spécifications en UML et B. Proc. AFADL'2000: Approches formelles dans l'assistance au développement de logiciels, Tech. rep. A00-R-009, LSR Laboratory, Grenoble, France, January 26-28, 2000.

[13]

Marcano-Kamenoff, R., Levy, N., Losavio, F.: Spécification et spécialisation de patterns en UML et B. Proc. LMO'2000: Langages et modèles à objets, Hermès Science Publications, Mont Saint-Hilaire, Québec, Canada, January 25-27, 2000.

[14]

Mikkonen, T.: Formalizing design patterns. Proc. of the 20th International Conference on Software Engineering, IEEE Computer Society, pages 115-124, Kyoto, Japan, April 19-25, 1998.

Digital Library

[15]

Nguyen, H.P.: Dérivation de spécifications formelles B à partir de spécifications semi-formelles. Ph.D. Thesis, CEDRIC Laboratory, CNAM, Évry, France, 1998. Available at http://www.iie.cnam.fr/~laleau/

[16]

Prieto-Diaz, R., Freeman, P.: Classifying software for reusability. IEEE Software, 4(1), pages 6-16, January 1987.

Digital Library

Cited By

Tikhonova U(2019)Reusable specification templates for defining dynamic semantics of DSLsSoftware and Systems Modeling (SoSyM)10.1007/s10270-017-0590-018:1(691-720)Online publication date: 1-Feb-2019
https://dl.acm.org/doi/10.1007/s10270-017-0590-0
Matichuk DMurray T(2012)Extensible specifications for automatic re-use of specifications and proofsProceedings of the 10th international conference on Software Engineering and Formal Methods10.1007/978-3-642-33826-7_23(333-341)Online publication date: 1-Oct-2012
https://dl.acm.org/doi/10.1007/978-3-642-33826-7_23
Filali-Amine MLawall J(2010)Development of a synchronous subset of AADLProceedings of the Second international conference on Abstract State Machines, Alloy, B and Z10.1007/978-3-642-11811-1_19(245-258)Online publication date: 22-Feb-2010
https://dl.acm.org/doi/10.1007/978-3-642-11811-1_19
Show More Cited By

Recommendations

An approach to precisely specifying the problem domain of design patterns

The problem domain of a design pattern describes the problem context in which the pattern can be applied. In general, determining the applicability of a pattern to a particular problem heavily relies on the knowledge and experience the developer has ...
Knowledge Acquisition and Integration on Specification Change-A Method for Systematic Reuse
APSEC '95: Proceedings of the Second Asia Pacific Software Engineering Conference

Our research goal is to construct an environment that mechanically supports human intellectual activities through software development with reuse. We propose a model of software development with systematic reuse in which the existent program can be ...
A Tool and a Formalism to Design and Apply Patterns
OOIS '02: Proceedings of the 8th International Conference on Object-Oriented. Information Systems

Patterns systems are becoming more and more numerous. They offer product patterns or process patterns of varied range and cover (analysis, design or implementation patterns, and general, domain or enterprise patterns). New application development ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

ZB'03: Proceedings of the 3rd international conference on Formal specification and development in Z and B

June 2003

546 pages

ISBN:3540402535

Editors:
Didier Bert
CNRS, Laboratoire LSR-IMAG, Saint-Martin-d'Heres Cedex, France
,
Jonathan P. Bowen
London South Bank University, London, UK
,
Steve King
University of York, Department of Computer Science, Heslington, York, UK
,
Marina Waldén
Åbo Akademi University, Department of Computer Science, Turku, Finland

Sponsors

FME
Z User Group
Nokia
ClearSy System Engineering
BCS-FACS

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 04 June 2003

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 22 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Tikhonova U(2019)Reusable specification templates for defining dynamic semantics of DSLsSoftware and Systems Modeling (SoSyM)10.1007/s10270-017-0590-018:1(691-720)Online publication date: 1-Feb-2019
https://dl.acm.org/doi/10.1007/s10270-017-0590-0
Matichuk DMurray T(2012)Extensible specifications for automatic re-use of specifications and proofsProceedings of the 10th international conference on Software Engineering and Formal Methods10.1007/978-3-642-33826-7_23(333-341)Online publication date: 1-Oct-2012
https://dl.acm.org/doi/10.1007/978-3-642-33826-7_23
Filali-Amine MLawall J(2010)Development of a synchronous subset of AADLProceedings of the Second international conference on Abstract State Machines, Alloy, B and Z10.1007/978-3-642-11811-1_19(245-258)Online publication date: 22-Feb-2010
https://dl.acm.org/doi/10.1007/978-3-642-11811-1_19
Ruhroth TWehrheim H(2009)Static Class Elements for Object-ZElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2009.12.025259(193-205)Online publication date: 1-Dec-2009
https://dl.acm.org/doi/10.1016/j.entcs.2009.12.025
Staines A(2008)Modeling UML software design patterns using fundamental modeling concepts (FMC)Proceedings of the 2nd conference on European computing conference10.5555/1562423.1562458(192-197)Online publication date: 11-Sep-2008
https://dl.acm.org/doi/10.5555/1562423.1562458

View Options

View options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents