Abstract
Formal methods still lack guidelines to construct models. We propose a systematic modelling approach to derive an event-based model of a system from the process-oriented models of its components. An extension of Mealy machines called polyadic Mealy machine is proposed, formalised and used to support the process-oriented view of local models that describe the components of a system. We show how event-based models can be derived from the process-oriented Mealy machines. The local process models are composed to build a global process-oriented model of the intended initial system, i.e., we derive systematically an event-based model from the composed system. The method is illustrated through the example of an auction system which is representative of a system without a static architecture: an evolving system. The resulting specification is augmented with desired properties and then analysed using the Event-B/Rodin framework. This method is well-suited to build Event-B models in general but also models with evolving architectures.
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
Notes
- 1.
- 2.
That combines state-machine and event-based notations.
- 3.
We use the set theoretic notation with the standard operators; the operator dom stands for the domain of a relation.
- 4.
\(\mathsf{guard}(\lambda )\) denotes the guard of a label.
- 5.
A process type is the set of behaviours that characterises a process.
- 6.
The term global state refers to the state of the process composition.
- 7.
A system behaviour is a discrete transition system.
- 8.
- 9.
Multi-process specification using B.
- 10.
As a type is a property, it is safe to write a guard \(p \in PT\) to express that p has the property PT.
- 11.
(See for example Rubis http://rubis.ow2.org/).
- 12.
References
Abadi, M., Lamport, L.: Conjoining specifications. ACM Trans. Program. Lang. Syst. 17(3), 507–535 (1995)
Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, New York (2010)
Attiogbé, C.: Event-based approach to modeling dynamic architecture: application to mobile adhoc network. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation, ISOLA 2008. CCIS, vol. 17, pp. 769–781. Springer, Heidelberg (2008)
Butler, M., Leuschel, M.: Combining CSP and B for specification and property verification. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 221–236. Springer, Heidelberg (2005)
Chen, B., Sadaoui, S.: Simulation and verification of a dynamic online auction. In: IASTED Conference on Software Engineering - SEA 2003 (2003)
Hillston, J., Kloul, L.: Performance investigation of an on-line auction system. Concurrency Comput. Pract. Experience 13(1), 23–41 (2001)
Hoang, T.S., Kuruma, H., Basin, D.A., Abrial, J.-R.: Developing topology discovery in Event-B. Sci. Comput. Program. 74(11–12), 879–899 (2009)
Milhau, J., Frappier, M., Gervais, F., Laleau, R.: Systematic translation rules from astd to Event-B. In: Méry, D., Merz, S. (eds.) IFM 2010. LNCS, vol. 6396, pp. 245–259. Springer, Heidelberg (2010)
Roth, C.H., Kinney, L.L.: Fundamentals of Logic Design. Thomson/Brooks/Cole, Belmont (2004)
Schneider, S., Treharne, H., Wehrheim, H.: A CSP approach to control in Event-B. In: Méry, D., Merz, S. (eds.) IFM 2010. LNCS, vol. 6396, pp. 260–274. Springer, Heidelberg (2010)
Zave, P., Jackson, M.: Conjunction as composition. ACM Trans. Softw. Eng. Methodol. 2(4), 379–411 (1993)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Attiogbé, C. (2015). Deriving Event-B Models from Mealy Machines: Application to an Auction System. In: Bellatreche, L., Manolopoulos, Y. (eds) Model and Data Engineering. Lecture Notes in Computer Science(), vol 9344. Springer, Cham. https://doi.org/10.1007/978-3-319-23781-7_7
Download citation
DOI: https://doi.org/10.1007/978-3-319-23781-7_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-23780-0
Online ISBN: 978-3-319-23781-7
eBook Packages: Computer ScienceComputer Science (R0)