Abstract
Scenarios of execution are commonly used to specify partial behaviour and interactions between different objects and components in a system. To avoid overall inconsistency in specifications, various automated methods have emerged in the literature to compose (behavioural) models. In recent work, we have shown how the theorem prover Isabelle can be combined with the constraint solver Z3 to efficiently detect inconsistencies in two or more behavioural models and, in their absence, generate the composition. Here, we extend our approach further and show how to generate the correct composition (as a set of valid traces) of dephased models. This work has been inspired by a problem from a medical domain where different care pathways (for chronic conditions) may be applied to the same patient with different starting points.
This research is supported by EPSRC grant EP/M014290/1.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Araújo, J., Whittle, J., Kim, D.: Modeling and composing scenario-based requirements with aspects. In: RE 2004, pp. 58–67. IEEE Computer Society Press (2004)
Bjørner, N., Phan, A.-D., Fleckenstein, L.: \(\nu \)z - An Optimizing SMT Solver. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 194–199. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46681-0_14
Bowles, J., Alwanain, M., Bordbar, B., Chen, Y.: Matching and Merging Scenarios Automatically with Alloy. In: Hammoudi, S., Pires, L.F., Filipe, J., das Neves, R.C. (eds.) MODELSWARD 2014. CCIS, vol. 506, pp. 100–116. Springer, Cham (2015). doi:10.1007/978-3-319-25156-1_7
Bowles, J.K.F., Bordbar, B., Alwanain, M.: A Logical Approach for Behavioural Composition of Scenario-Based Models. In: Butler, M., Conchon, S., Zaïdi, F. (eds.) ICFEM 2015. LNCS, vol. 9407, pp. 252–269. Springer, Cham (2015). doi:10.1007/978-3-319-25423-4_16
Bowles, J.K.F.: Decomposing Interactions. In: Johnson, M., Vene, V. (eds.) AMAST 2006. LNCS, vol. 4019, pp. 189–203. Springer, Heidelberg (2006). doi:10.1007/11784180_16
Bowles, J., Bordbar, B.: A formal model for integrating multiple views. In: ACSD 2007, pp. 71–79. IEEE Computer Society Press (2007)
Bowles, J., Bordbar, B., Alwanain, M.: Weaving true-concurrent aspects using constraint solvers. In: Application of Concurrency to System Design (ACSD 2016). IEEE Computer Society Press, June 2016
Bowles, J.K.F., Caminati, M.B.: Mind the gap: addressing behavioural inconsistencies with formal methods. In: 23rd Asia-Pacific Software Engineering Conference (APSEC). IEEE Computer Society (2016)
D’Ippolito, N., Frias, M.F., Galeotti, J.P., Lanzarotti, E., Mera, S.: Alloy+HotCore: A Fast Approximation to Unsat Core. In: Frappier, M., Glässer, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) ABZ 2010. LNCS, vol. 5977, pp. 160–173. Springer, Heidelberg (2010). doi:10.1007/978-3-642-11811-1_13
Harel, D., Marelly, R.: Come, Let’s Play. Scenario-based Programming Using LSCs and the Play-Engine. Springer, Heidelberg (2003)
Jackson, D.: Software Abstractions: Logic, Language and Analysis. MIT Press, Cambridge (2006)
Klein, J., Hélouët, L., Jézéquel, J.: Semantic-based weaving of scenarios. In: AOSD 2006, pp. 27–38. ACM (2006)
Kovalov, A., Bowles, J.K.F.: Avoiding Medication Conflicts for Patients with Multimorbidities. In: Ábrahám, E., Huisman, M. (eds.) IFM 2016. LNCS, vol. 9681, pp. 376–390. Springer, Cham (2016). doi:10.1007/978-3-319-33693-0_24
Küster-Filipe, J.: Modelling concurrent interactions. Theoret. Comput. Sci. 351, 203–220 (2006)
Liang, H., Diskin, Z., Dingel, J., Posse, E.: A General Approach for Scenario Integration. In: Czarnecki, K., Ober, I., Bruel, J.-M., Uhl, A., Völter, M. (eds.) MODELS 2008. LNCS, vol. 5301, pp. 204–218. Springer, Heidelberg (2008). doi:10.1007/978-3-540-87875-9_15
de Moura, L., Bjørner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). doi:10.1007/978-3-540-78800-3_24
Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle/HOL–A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)
OMG: Business Process Model and Notation. Version 2.0. OMG, documentid: formal/2011-01-03 (2011). http://www.omg.org
OMG: UML: Superstructure. Version 2.4.1. OMG, documentid: formal/2011-08-06 (2011). http://www.omg.org
Reddy, R., Solberg, A., France, R., Ghosh, S.: Composing sequence models using tags. In: Proceedings of MoDELS Workshop on Aspect Oriented Modeling (2006)
Rubin, J., Chechik, M., Easterbrook, S.: Declarative approach for model composition. In: MiSE 2008, pp. 7–14. ACM (2008)
Uchitel, S., Brunet, G., Chechik, M.: Synthesis of partial behavior models from properties and scenarios. IEEE Trans. Software Eng. 35(3), 384–406 (2009)
Whittle, J., Araújo, J., Moreira, A.: Composing aspect models with graph transformations. In: Proceedings of the 2006 International Workshop on Early Aspects at ICSE, pp. 59–65. ACM (2006)
Widl, M., Biere, A., Brosch, P., Egly, U., Heule, M., Kappel, G., Seidl, M., Tompits, H.: Guided Merging of Sequence Diagrams. In: Czarnecki, K., Hedin, G. (eds.) SLE 2012. LNCS, vol. 7745, pp. 164–183. Springer, Heidelberg (2013). doi:10.1007/978-3-642-36089-3_10
Winskel, G., Nielsen, M.: Models for Concurrency. In: Abramsky, S., Gabbay, D., Maibaum, T. (eds.) Handbook of Logic in Computer Science: Semantic Modelling, vol. 4, pp. 1–148. Oxford Science Publications, Oxford (1995)
Zhang, D., Li, S., Liu, X.: An approach for model composition and verification. In: NCM 2009, pp. 1102–1107. IEEE Computer Society Press (2009)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Bowles, J., Caminati, M.B. (2017). Correct Composition of Dephased Behavioural Models. In: Proença, J., Lumpe, M. (eds) Formal Aspects of Component Software. FACS 2017. Lecture Notes in Computer Science(), vol 10487. Springer, Cham. https://doi.org/10.1007/978-3-319-68034-7_14
Download citation
DOI: https://doi.org/10.1007/978-3-319-68034-7_14
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-68033-0
Online ISBN: 978-3-319-68034-7
eBook Packages: Computer ScienceComputer Science (R0)