Formalising the Dezyne modelling language in mCRL2

R. van Beusekom; J.F. Groote; P. Hoogendijk; R. Howe; W. Wesselink; R. Wieringa; T.A.C. Willemse

doi:10.1007/978-3-319-67113-0_14

Formalising the Dezyne modelling language in mCRL2

R. van Beusekom, J.F. Groote, P. Hoogendijk, R. Howe, W. Wesselink, R. Wieringa, T.A.C. Willemse

Formal System Analysis

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

10 Citations (Scopus)

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.

Original language	English
Title of host publication	Critical Systems: Formal Methods and Automated Verification
Subtitle of host publication	Joint 22nd International Workshop on Formal Methods for Industrial Critical Systems and 17th International Workshop on Automated Verification of Critical Systems, FMICS-AVoCS 2017, Turin, Italy, September 18–20, 2017, Proceedings
Editors	L. Petrucci, C. Seceleanu, A. Cavalcanti
Place of Publication	Dordrecht
Publisher	Springer
Pages	217-233
Number of pages	17
ISBN (Electronic)	978-3-319-67113-0
ISBN (Print)	978-3-319-67112-3
DOIs	https://doi.org/10.1007/978-3-319-67113-0_14
Publication status	Published - 2017
Event	22nd International Workshop on Formal Methods for Industrial Critical Systems and 17th International Workshop on Automated Verification of Critical Systems, FMICS-AVoCS 2017 - Turin, Italy Duration: 18 Sept 2017 → 20 Sept 2017

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	10471 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	22nd International Workshop on Formal Methods for Industrial Critical Systems and 17th International Workshop on Automated Verification of Critical Systems, FMICS-AVoCS 2017
Country/Territory	Italy
City	Turin
Period	18/09/17 → 20/09/17

Access to Document

10.1007/978-3-319-67113-0_14

Cite this

van Beusekom, R., Groote, J. F., Hoogendijk, P., Howe, R., Wesselink, W., Wieringa, R., & Willemse, T. A. C. (2017). Formalising the Dezyne modelling language in mCRL2. In L. Petrucci, C. Seceleanu, & A. Cavalcanti (Eds.), Critical Systems: Formal Methods and Automated Verification: Joint 22nd International Workshop on Formal Methods for Industrial Critical Systems and 17th International Workshop on Automated Verification of Critical Systems, FMICS-AVoCS 2017, Turin, Italy, September 18–20, 2017, Proceedings (pp. 217-233). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10471 LNCS). Springer. https://doi.org/10.1007/978-3-319-67113-0_14

van Beusekom, R. ; Groote, J.F. ; Hoogendijk, P. et al. / Formalising the Dezyne modelling language in mCRL2. Critical Systems: Formal Methods and Automated Verification: Joint 22nd International Workshop on Formal Methods for Industrial Critical Systems and 17th International Workshop on Automated Verification of Critical Systems, FMICS-AVoCS 2017, Turin, Italy, September 18–20, 2017, Proceedings. editor / L. Petrucci ; C. Seceleanu ; A. Cavalcanti. Dordrecht : Springer, 2017. pp. 217-233 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{1f39afd839c04f4e85bdfd0bf9f1e819,

title = "Formalising the Dezyne modelling language in mCRL2",

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

author = "{van Beusekom}, R. and J.F. Groote and P. Hoogendijk and R. Howe and W. Wesselink and R. Wieringa and T.A.C. Willemse",

year = "2017",

doi = "10.1007/978-3-319-67113-0_14",

language = "English",

isbn = "978-3-319-67112-3",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "217--233",

editor = "L. Petrucci and C. Seceleanu and A. Cavalcanti",

booktitle = "Critical Systems: Formal Methods and Automated Verification",

address = "Germany",

note = "22nd International Workshop on Formal Methods for Industrial Critical Systems and 17th International Workshop on Automated Verification of Critical Systems, FMICS-AVoCS 2017 ; Conference date: 18-09-2017 Through 20-09-2017",

}

van Beusekom, R, Groote, JF, Hoogendijk, P, Howe, R, Wesselink, W, Wieringa, R & Willemse, TAC 2017, Formalising the Dezyne modelling language in mCRL2. in L Petrucci, C Seceleanu & A Cavalcanti (eds), Critical Systems: Formal Methods and Automated Verification: Joint 22nd International Workshop on Formal Methods for Industrial Critical Systems and 17th International Workshop on Automated Verification of Critical Systems, FMICS-AVoCS 2017, Turin, Italy, September 18–20, 2017, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10471 LNCS, Springer, Dordrecht, pp. 217-233, 22nd International Workshop on Formal Methods for Industrial Critical Systems and 17th International Workshop on Automated Verification of Critical Systems, FMICS-AVoCS 2017, Turin, Italy, 18/09/17. https://doi.org/10.1007/978-3-319-67113-0_14

Formalising the Dezyne modelling language in mCRL2. / van Beusekom, R.; Groote, J.F.; Hoogendijk, P. et al.

Critical Systems: Formal Methods and Automated Verification: Joint 22nd International Workshop on Formal Methods for Industrial Critical Systems and 17th International Workshop on Automated Verification of Critical Systems, FMICS-AVoCS 2017, Turin, Italy, September 18–20, 2017, Proceedings. ed. / L. Petrucci; C. Seceleanu; A. Cavalcanti. Dordrecht : Springer, 2017. p. 217-233 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10471 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Formalising the Dezyne modelling language in mCRL2

AU - van Beusekom, R.

AU - Groote, J.F.

AU - Hoogendijk, P.

AU - Howe, R.

AU - Wesselink, W.

AU - Wieringa, R.

AU - Willemse, T.A.C.

PY - 2017

Y1 - 2017

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

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

UR - http://www.scopus.com/inward/record.url?scp=85029487269&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-67113-0_14

DO - 10.1007/978-3-319-67113-0_14

M3 - Conference contribution

AN - SCOPUS:85029487269

SN - 978-3-319-67112-3

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 217

EP - 233

BT - Critical Systems: Formal Methods and Automated Verification

A2 - Petrucci, L.

A2 - Seceleanu, C.

A2 - Cavalcanti, A.

PB - Springer

CY - Dordrecht

T2 - 22nd International Workshop on Formal Methods for Industrial Critical Systems and 17th International Workshop on Automated Verification of Critical Systems, FMICS-AVoCS 2017

Y2 - 18 September 2017 through 20 September 2017

ER -

van Beusekom R, Groote JF, Hoogendijk P, Howe R, Wesselink W, Wieringa R et al. Formalising the Dezyne modelling language in mCRL2. In Petrucci L, Seceleanu C, Cavalcanti A, editors, Critical Systems: Formal Methods and Automated Verification: Joint 22nd International Workshop on Formal Methods for Industrial Critical Systems and 17th International Workshop on Automated Verification of Critical Systems, FMICS-AVoCS 2017, Turin, Italy, September 18–20, 2017, Proceedings. Dordrecht: Springer. 2017. p. 217-233. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-67113-0_14

Formalising the Dezyne modelling language in mCRL2

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

FMICS-AVoCS Best Paper award

Cite this

Formalising the Dezyne modelling language in mCRL2

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Prizes

FMICS-AVoCS Best Paper award

Cite this