Skip to main content
SpringerLink
Log in

Formalising the Dezyne Modelling Language in mCRL2

  • Conference paper
  • First Online:
Book cover Critical Systems: Formal Methods and Automated Verification (AVoCS 2017, FMICS 2017)

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

Abstract

Dezyne is an industrial language with an associated set of tools, allowing users to model interface behaviours and implementations of reactive components and generate executable code from these. The tool and language succeed the successful ASD:Suite tool set, which, in addition to modelling reactive components, offers a set of verification capabilities allowing users to check the conformance of implementations to their interfaces. In this paper, we describe the Dezyne language and a model transformation to the mCRL2 language, providing users access to advanced model checking capabilities and refinement checks of the mCRL2 tool set.

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

Notes

  1. 1.

    See https://www.verum.com; accessed 21 May 2017.

  2. 2.

    The option to check for this refinement relation, and other refinement relations such as trace inclusion, weak trace inclusion, failures, weak failures and simulation preorder is available from mCRL2 revision 13875 and onward. The additions weigh in at approximately 800 lines of code, which include, among others the additional algorithms and test cases for these algorithms.

  3. 3.

    Unfortunately, we cannot disclose the origin of, nor further details about these industrial models.

References

  1. Baeten, J.C.M., Basten, T., Reniers, M.A.: Process Algebra: Equational Theories of Communicating Processes. Cambridge Tracts in Theoretical Computer Science, vol. 50. Cambridge University Press, New York (2010)

    MATH  Google Scholar 

  2. Clinger, W.D.: Proper tail recursion and space efficiency. In: PLDI, pp. 174–185. ACM (1998)

    Google Scholar 

  3. Cranen, S., Groote, J.F., Keiren, J.J.A., Stappers, F.P.M., Vink, E.P., Wesselink, W., Willemse, T.A.C.: An overview of the mCRL2 toolset and its recent advances. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 199–213. Springer, Heidelberg (2013). doi:10.1007/978-3-642-36742-7_15

    Chapter  Google Scholar 

  4. Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3: a parallel refinement checker for CSP. Int. J. Softw. Tools Technol. Transf. 18(2), 149–167 (2016)

    Article  Google Scholar 

  5. Groote, J.F., Mousavi, M.R.: Modeling and Analysis of Communicating Systems. MIT Press, Cambridge (2014)

    MATH  Google Scholar 

  6. Roscoe, A.W.: On the expressive power of CSP refinement. Formal Asp. Comput. 17(2), 93–112 (2005)

    Article  MATH  Google Scholar 

  7. Wang, T., Song, S., Sun, J., Liu, Y., Dong, J.S., Wang, X., Li, S.: More anti-chain based refinement checking. In: Aoki, T., Taguchi, K. (eds.) ICFEM 2012. LNCS, vol. 7635, pp. 364–380. Springer, Heidelberg (2012). doi:10.1007/978-3-642-34281-3_26

    Chapter  Google Scholar 

Download references

Acknowledgements

Wieger Wesselink and Tim Willemse were funded by the EU-FP7 TTP VICTORIA project (project grant agreement 609491).

Author information

Authors and Affiliations

  1. Eindhoven University of Technology, Eindhoven, The Netherlands

    Jan Friso Groote, Wieger Wesselink & Tim A. C. Willemse

  2. Verum Software Tools B.V., Waalre, The Netherlands

    Rutger van Beusekom, Paul Hoogendijk, Robert Howe & Rob Wieringa

Authors
  1. Rutger van Beusekom
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jan Friso Groote
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Paul Hoogendijk
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Robert Howe
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Rob Wieringa
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Tim A. C. Willemse
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Tim A. C. Willemse .

Editor information

Editors and Affiliations

  1. Paris 13 University, Villetaneuse, France

    Laure Petrucci

  2. Mälardalen University, Västerås, Sweden

    Cristina Seceleanu

  3. University of York, York, United Kingdom

    Ana Cavalcanti

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

van Beusekom, R. et al. (2017). Formalising the Dezyne Modelling Language in mCRL2. In: Petrucci, L., Seceleanu, C., Cavalcanti, A. (eds) Critical Systems: Formal Methods and Automated Verification. AVoCS FMICS 2017 2017. Lecture Notes in Computer Science(), vol 10471. Springer, Cham. https://doi.org/10.1007/978-3-319-67113-0_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-67113-0_14

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-67112-3

  • Online ISBN: 978-3-319-67113-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation