Abstract
Event-B is a formal method, based on set theory and first-order logic, for specification and verification of reactive systems supported by the Rodin tool kit. Feature modelling is a well-known technique for managing variability and configuring products within software product lines (SPLs). Our objective is to explore whether we can use existing Event-B composition techniques and tooling for feature-based product line development. If case-study experiments reveal these mechanisms to be inadequate, then they also should suggest further research directions. The main objective is to maximise the amount of reuse. This includes avoiding as far as possible having to reprove a composed specification when the models being composed have already been proven. We have modelled two case-studies in Event-B using both horizontal and vertical refinements. This work contributes by analysing existing tools and techniques in Event-B for feature-based development, exploring composition related issues by modelling example case-studies and suggesting further tooling requirements.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abrial, J.R.: Modeling in Event-B: System and Software Engineering, 1st edn., Cambridge University Press, Cambridge (2010)
Abrial, J.R.: The B-book: assigning programs to meanings. Cambridge University Press, New York (1996)
Clements, P., Northrop, L.: Software Product Lines: Practices and Patterns. Addison-Wesley Professional, Reading (2001)
Lee, K., Kang, K.C., Lee, J.J.: Concepts and guidelines of feature modeling for product line software engineering. In: Gacek, C. (ed.) ICSR 2002. LNCS, vol. 2319, pp. 62–77. Springer, Heidelberg (2002)
Bosch, J.: Design and use of software architectures: adopting and evolving a product-line approach. ACM Press/Addison-Wesley (2000)
Snook, C., Poppleton, M., Johnson, I.: Rigorous engineering of product-line requirements: a case study in failure management. IST 50(1-2), 112–129 (2008)
Abrial, J.R., Hallerstede, S.: Refinement, Decomposition, and Instantiation of Discrete Models: Application to Event-B. Fundam. Inf. 77(1-2), 1–28 (2007)
Butler, M.: Synchronisation-based Decomposition for Event-B. In: RODIN Deliverable D19 Intermediate report on methodology (2006)
Hoare, C.A.R.: Communicating sequential processes. Prentice-Hall, Inc., Upper Saddle River (1985)
Back, R., von Wright, J.: Trace refinement of action systems. In: Jonsson, B., Parrow, J. (eds.) CONCUR 1994. LNCS, vol. 836, pp. 367–384. Springer, Heidelberg (1994)
Silva, R., Pascal, C., Hoang, T.S., Butler, M.: Decomposition tool for event-b. In: Workshop on Tool Building in Formal Methods - ABZ Conference (January 2010)
Poppleton, M.R.: The composition of event-B models. In: Börger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol. 5238, pp. 209–222. Springer, Heidelberg (2008)
Gondal, A., Poppleton, M., Snook, C.: Feature composition - towards product lines of Event-B models. In: MDPLE 2009 CTIT Workshop Proceedings (June 2009)
Gondal, A., Poppleton, M., Butler, M., Snook, C.: Feature-Oriented Modelling Using Event-B. In: SETP-10, Orlando, FL, USA (2010)
Czarnecki, K., Helsen, S., Eisenecker, U.: Staged configuration through specialization and multilevel configuration of feature models. Software Process: Improvement and Practice 10(2), 143–169 (2005)
Lindner, T.: Task description. In: Lewerentz, C., Lindner, T. (eds.) Formal Development of Reactive Systems. LNCS, vol. 891, Springer, Heidelberg (1995)
Butler, M.: Towards a cookbook for modelling and refinement of control problems (2009), http://deploy-eprints.ecs.soton.ac.uk/108/
Kishi, T., Noda, N.: Formal verification and software product lines. Commun. ACM 49(0001-0782), 73–77 (2006)
Clarke, D., Diakov, N., Hähnle, R., Johnsen, E.B., Puebla, G., Weitzel, B., Wong, P.Y.H.: HATS-a formal software product line engineering methodology. In: Proc. Intl. Workshop on Formal Methods in SPL Engineering, South Corea (2010)
Lau, K.K., Wang, Z., Wang, A., Gu, M.: A component-based approach to verified software: What, why, how and what next? In: Chen, X., Liu, Z., Reed, M. (eds.) Proc. 1st Asian Working Conference on Verified Software, pp. 225–229 (2006)
Sorge, J., Poppleton, M., Butler, M.: A basis for feature-oriented modelling in event-B. In: Frappier, M., Glässer, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) ABZ 2010. LNCS, vol. 5977, pp. 409–409. Springer, Heidelberg (2010)
Apel, S., Kastner, C., Lengauer, C.: FEATUREHOUSE: Language-independent, automated software composition. In: ICSE 2009, USA, pp. 221–231 (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gondal, A., Poppleton, M., Butler, M. (2011). Composing Event-B Specifications - Case-Study Experience. In: Apel, S., Jackson, E. (eds) Software Composition. SC 2011. Lecture Notes in Computer Science, vol 6708. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-22045-6_7
Download citation
DOI: https://doi.org/10.1007/978-3-642-22045-6_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-22044-9
Online ISBN: 978-3-642-22045-6
eBook Packages: Computer ScienceComputer Science (R0)