Abstract
Traces are used to show whether a model complies with the intended behavior. A modeler can use trace checking to ensure the preservation of the model behavior during the refinement process. In this paper, we present a trace refinement technique and tool called BERT that allows designers to ensure the behavioral integrity of high-level traces at the concrete level. The proposed technique is evaluated within the context of the B and Event-B methods on industrial-strength case studies from the automotive domain.
This research presented in this paper has been conducted within the IVOIRE project, which is funded by “Deutsche Forschungsgemeinschaft” (DFG) and the Austrian Science Fund (FWF) grant # I 4744-N. The work of Austrian authors has been partly funded by the LIT Secure and Correct Systems Lab sponsored by the province of Upper Austria.
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
Similar content being viewed by others
Notes
- 1.
In the following, events and operations will be used as interchangeable words.
- 2.
We model them in the way how German traffic lights operate.
- 3.
The graphical output shown in Fig. 1d is the result of BERT’s automatic visualization. As ProBs internal representation is used, some names, for example \(initalize\_machine\), are held in the ProB style.
- 4.
BERT is available as part of ProB2, see https://www3.hhu.de/stups/downloads/prob2/snapshot/.
- 5.
A demo is provided at https://doi.org/10.6084/m9.figshare.16909006.v2.
References
Abrial, J.R.: The B-book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (2005)
Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)
Abrial, J.R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. Int. J. Softw. Tools Technol. Transfer 12(6), 447–466 (2010). https://doi.org/10.1007/s10009-010-0145-y
Arcaini, P., Riccobene, E.: Automatic refinement of ASM abstract test cases. In: 2019 IEEE International Conference on Software Testing, Verification and Validation Workshops (ICSTW), pp. 1–10 (2019)
Back, R.J.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). https://doi.org/10.1007/978-3-540-48654-1_28
Bendisposto, J., et al.: ProB2-UI: a Java-based user interface for ProB. In: Lluch Lafuente, A., Mavridou, A. (eds.) FMICS 2021. LNCS, vol. 12863, pp. 193–201. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-85248-1_12
Butler, M.: An approach to the design of distributed systems with B AMN. In: Bowen, J.P., Hinchey, M.G., Till, D. (eds.) ZUM 1997. LNCS, vol. 1212, pp. 221–241. Springer, Heidelberg (1997). https://doi.org/10.1007/BFb0027291
Derrick, J., Boiten, E.: Refinement: Semantics, Languages and Applications. Springer, Heidelberg (2018). https://doi.org/10.1007/978-3-319-92711-4
Dunne, S., Conroy, S.: Process refinement in B. In: Treharne, H., King, S., Henson, M., Schneider, S. (eds.) ZB 2005. LNCS, vol. 3455, pp. 45–64. Springer, Heidelberg (2005). https://doi.org/10.1007/11415787_4
Rodin User’s Handbook. https://www3.hhu.de/stups/handbook/rodin/current/html/. Accessed 12 Sep 2022
Fischer, T., Dghyam, D.: Formal model validation through acceptance tests. In: Collart-Dutilleul, S., Lecomte, T., Romanovsky, A. (eds.) RSSRail 2019. LNCS, vol. 11495, pp. 159–169. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-18744-6_10
Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3 — a modern refinement checker for CSP. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 187–201. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54862-8_13
Hallerstede, S., Leuschel, M., Plagge, D.: Refinement-animation for Event-B — towards a method of validation. In: Frappier, M., Glässer, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) ABZ 2010. LNCS, vol. 5977, pp. 287–301. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-11811-1_22
Hallerstede, S., Leuschel, M., Plagge, D.: Validation of formal models by refinement animation. Sci. Comput. Program. 78(3), 272–292 (2013)
Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666–677 (1978)
Houdek, F., Raschke, A.: Adaptive exterior light and speed control system. In: Raschke, A., Méry, D., Houdek, F. (eds.) ABZ 2020. LNCS, vol. 12071, pp. 281–301. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-48077-6_24
Leuschel, M.: Spot the difference: a detailed comparison between B and Event-B. In: Raschke, A., Riccobene, E., Schewe, K.-D. (eds.) Logic, Computation and Rigorous Methods. LNCS, vol. 12750, pp. 147–172. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-76020-5_9
Leuschel, M., Butler, M.: Automatic refinement checking for B. In: Lau, K.-K., Banach, R. (eds.) ICFEM 2005. LNCS, vol. 3785, pp. 345–359. Springer, Heidelberg (2005). https://doi.org/10.1007/11576280_24
Leuschel, M., Butler, M.: ProB: an automated analysis toolset for the B method. Int. J. Softw. Tools Technol. Transfer 10(2), 185–203 (2008)
Leuschel, M., Mutz, M., Werth, M.: Modelling and validating an automotive system in classical B and Event-B. In: Raschke, A., Méry, D., Houdek, F. (eds.) ABZ 2020. LNCS, vol. 12071, pp. 335–350. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-48077-6_27
Malik, Q.A., Lilius, J., Laibinis, L.: Model-based testing using scenarios and Event-B refinements. In: Butler, M., Jones, C., Romanovsky, A., Troubitsyna, E. (eds.) Methods, Models and Tools for Fault Tolerance. LNCS, vol. 5454, pp. 177–195. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-00867-2_9
Mammar, A., Frappier, M., Laleau, R.: An Event-B model of an automotive adaptive exterior light system. In: Raschke, A., Méry, D., Houdek, F. (eds.) ABZ 2020. LNCS, vol. 12071, pp. 351–366. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-48077-6_28
Mashkoor, A., Jacquot, J.P.: Guidelines for formal domain modeling in Event-B. In: 2011 IEEE 13th International Symposium on High-Assurance Systems Engineering, pp. 138–145 (2011)
Mashkoor, A., Jacquot, J.: Utilizing Event-B for domain engineering: a critical analysis. Requir. Eng. 16(3), 191–207 (2011)
Mashkoor, A., Kossak, F., Egyed, A.: Evaluating the suitability of state-based formal methods for industrial deployment. Softw. Pract. Exp. 48(12), 2350–2379 (2018)
Mashkoor, A., Leuschel, M., Egyed, A.: Validation obligations: a novel approach to check compliance between requirements and their formal specification. In: 2021 IEEE/ACM 43rd International Conference on Software Engineering: New Ideas and Emerging Results (ICSE-NIER), pp. 1–5 (2021)
Snook, C., Hoang, T.S., Dghaym, D., Fathabadi, A.S., Butler, M.: Domain-specific scenarios for refinement-based methods. J. Syst. Architect. 112, 101833 (2021)
Snook, C., Hoang, T.S., Fathabadi, A.S., Dghaym, D., Butler, M.: Scenario checker: an Event-B tool forvalidating abstract models. In: Rodin Workshop (2021)
Wynne, M., Hellesoy, A., Tooke, S.: The Cucumber Book: Behaviour-driven Development for Testers and Developers. Pragmatic Bookshelf (2017)
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2022 Springer Nature Switzerland AG
About this paper
Cite this paper
Stock, S., Mashkoor, A., Leuschel, M., Egyed, A. (2022). Trace Refinement in B and Event-B. In: Riesco, A., Zhang, M. (eds) Formal Methods and Software Engineering. ICFEM 2022. Lecture Notes in Computer Science, vol 13478. Springer, Cham. https://doi.org/10.1007/978-3-031-17244-1_19
Download citation
DOI: https://doi.org/10.1007/978-3-031-17244-1_19
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-17243-4
Online ISBN: 978-3-031-17244-1
eBook Packages: Computer ScienceComputer Science (R0)