Skip to main content
SpringerLink
Log in

Correct Composition of Dephased Behavioural Models

  • Conference paper
  • First Online:
Formal Aspects of Component Software (FACS 2017)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10487))

Included in the following conference series:

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. 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)

    Google Scholar 

  2. 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

    Google Scholar 

  3. 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

    Chapter  Google Scholar 

  4. 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

    Chapter  Google Scholar 

  5. 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

    Chapter  Google Scholar 

  6. Bowles, J., Bordbar, B.: A formal model for integrating multiple views. In: ACSD 2007, pp. 71–79. IEEE Computer Society Press (2007)

    Google Scholar 

  7. 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

    Google Scholar 

  8. 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)

    Google Scholar 

  9. 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

    Chapter  Google Scholar 

  10. Harel, D., Marelly, R.: Come, Let’s Play. Scenario-based Programming Using LSCs and the Play-Engine. Springer, Heidelberg (2003)

    Book  Google Scholar 

  11. Jackson, D.: Software Abstractions: Logic, Language and Analysis. MIT Press, Cambridge (2006)

    Google Scholar 

  12. Klein, J., Hélouët, L., Jézéquel, J.: Semantic-based weaving of scenarios. In: AOSD 2006, pp. 27–38. ACM (2006)

    Google Scholar 

  13. 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

    Chapter  Google Scholar 

  14. Küster-Filipe, J.: Modelling concurrent interactions. Theoret. Comput. Sci. 351, 203–220 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  15. 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

    Chapter  Google Scholar 

  16. 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

    Chapter  Google Scholar 

  17. Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle/HOL–A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)

    MATH  Google Scholar 

  18. OMG: Business Process Model and Notation. Version 2.0. OMG, documentid: formal/2011-01-03 (2011). http://www.omg.org

  19. OMG: UML: Superstructure. Version 2.4.1. OMG, documentid: formal/2011-08-06 (2011). http://www.omg.org

  20. Reddy, R., Solberg, A., France, R., Ghosh, S.: Composing sequence models using tags. In: Proceedings of MoDELS Workshop on Aspect Oriented Modeling (2006)

    Google Scholar 

  21. Rubin, J., Chechik, M., Easterbrook, S.: Declarative approach for model composition. In: MiSE 2008, pp. 7–14. ACM (2008)

    Google Scholar 

  22. Uchitel, S., Brunet, G., Chechik, M.: Synthesis of partial behavior models from properties and scenarios. IEEE Trans. Software Eng. 35(3), 384–406 (2009)

    Article  Google Scholar 

  23. 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)

    Google Scholar 

  24. 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

    Chapter  Google Scholar 

  25. 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)

    Google Scholar 

  26. Zhang, D., Li, S., Liu, X.: An approach for model composition and verification. In: NCM 2009, pp. 1102–1107. IEEE Computer Society Press (2009)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Computer Science, University of St Andrews, KY16 9SX St Andrews, St Andrews, UK

    Juliana Bowles & Marco B. Caminati

Authors
  1. Juliana Bowles
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Marco B. Caminati
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Marco B. Caminati .

Editor information

Editors and Affiliations

  1. University of Minho, Braga, Portugal

    José Proença

  2. Swinburne University of Technology, Hawthorn, Victoria, Australia

    Markus Lumpe

Rights and permissions

Reprints 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)

Publish with us

Policies and ethics

Search

Navigation