Formalising the Dezyne modelling language in mCRL2

Autor: van Beusekom, R., Groote, J.F., Hoogendijk, P., Howe, R., Wesselink, W., Wieringa, R., Willemse, T.A.C., Petrucci, L., Seceleanu, C., Cavalcanti, A.

Publikováno v: 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, 217-233
STARTPAGE=217;ENDPAGE=233;TITLE=Critical Systems: Formal Methods and Automated Verification
Lecture Notes in Computer Science ISBN: 9783319671123
FMICS-AVoCS

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

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::9a6b2bb8afb2beb9ba93a494a5492c83
https://doi.org/10.1007/978-3-319-67113-0_14

An O(m log n) algorithm for stuttering equivalence and branching bisimulation

Autor: Groote, J.F., Wijs, A.J., Chechik, M., Raskin, J.-F.

Publikováno v: Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783662496732
TACAS
Tools and Algorithms for the Construction and Analysis of Systems: 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, 607-624
STARTPAGE=607;ENDPAGE=624;TITLE=Tools and Algorithms for the Construction and Analysis of Systems

We provide a new algorithm to determine stuttering equivalence with time complexity $$Om \log n$$, where n is the number of states and m is the number of transitions of a Kripke structure. This algorithm can also be used to determine branching bisimu

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::3cf02b61a4d0e9b642b1eb3bd154549d
http://www.scopus.com/inward/record.url?scp=84964057222&partnerID=8YFLogxK

Solving parameterised Boolean equation systems with infinite data through quotienting

Autor: Neele, T.S., Willemse, T.A.C., Groote, J.F.

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=narcis______::a467f3334dbb68a8e51f1a62ee185940
https://research.tue.nl/nl/publications/99bdb3e8-dd8b-4e0b-bef4-83534b25ae5e

Modeling and Verification of the Bitcoin Protocol

Autor: Chaudhary, Kaylash, Fehnker, Ansgar, van de Pol, Jan Cornelis, Stoelinga, Mariëlle Ida Antoinette, van Glabbeek, R.J., Groote, J.F., Höfner, P.

Publikováno v: Electronic Proceedings in Theoretical Computer Science, Vol 196, Iss Proc. MARS 2015, Pp 46-60 (2015)
Proceedings of the Workshop on Models for Formal Analysis of Real Systems (MARS 2015), 46-60
STARTPAGE=46;ENDPAGE=60;TITLE=Proceedings of the Workshop on Models for Formal Analysis of Real Systems (MARS 2015)

Bitcoin is a popular digital currency for online payments, realized as a decentralized peer-to-peer electronic cash system. Bitcoin keeps a ledger of all transactions; the majority of the participants decides on the correct ledger. Since there is no

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::834244f73125c184b5726f3b419828d0
https://doi.org/10.4204/eptcs.196.5

Modelling and Verification of a Cluster-tree Formation Protocol Implementation for the IEEE 802.15.4 TSCH MAC Operation Mode

Autor: Talebi, M., Groote, J.F., Dandelski, C., Hermanns, Holger, Höfner, Peter H.

Publikováno v: Electronic Proceedings in Theoretical Computer Science, Vol 244, Iss Proc. MARS 2017, Pp 117-128 (2017)
Proceedings 2nd Workshop on Models for Formal Analysis of Real Systems (MARS 2017), 117-128
STARTPAGE=117;ENDPAGE=128;TITLE=Proceedings 2nd Workshop on Models for Formal Analysis of Real Systems (MARS 2017)

Correct and efficient initialization of wireless sensor networks can be challenging in the face of many uncertainties present in ad hoc wireless networks. In this paper we examine an implementation for the formation of a cluster-tree topology in a ne

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::6043740b31d557a332c65bf307c1d7e7
http://arxiv.org/abs/1703.06572