{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,6]],"date-time":"2026-03-06T22:22:57Z","timestamp":1772835777840,"version":"3.50.1"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319989372","type":"print"},{"value":"9783319989389","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-98938-9_23","type":"book-chapter","created":{"date-parts":[[2018,8,8]],"date-time":"2018-08-08T11:08:34Z","timestamp":1533726514000},"page":"398-418","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Analysing AWN-Specifications Using mCRL2 (Extended Abstract)"],"prefix":"10.1007","author":[{"given":"Rob","family":"van Glabbeek","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"H\u00f6fner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Djurre","family":"van der Wal","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,8,9]]},"reference":[{"key":"23_CR1","doi-asserted-by":"publisher","unstructured":"Behrmann, G., David, A., Larsen, K.G., Pettersson, P., Wang Yi: Developing Uppaal over 15 years. Softw. - Pract. Exp. 41(2), 133\u2013142 (2011). https:\/\/doi.org\/10.1002\/spe.1006","DOI":"10.1002\/spe.1006"},{"key":"23_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-540-30080-9_7","volume-title":"Formal Methods for the Design of Real-Time Systems","author":"G Behrmann","year":"2004","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200\u2013236. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30080-9_7"},{"key":"23_CR3","unstructured":"Bergstra, J.A., Klop, J.W.: Algebra of communicating processes. In: de Bakker, Hazewinkel, J.W., Lenstra, J.K. (eds.) Mathematics and Computer Science, CWI Monograph 1, pp. 89\u2013138. North-Holland (1986)"},{"key":"23_CR4","volume-title":"Implementing Domain-Specific Languages with Xtext and Xtend","author":"L Bettini","year":"2016","unstructured":"Bettini, L.: Implementing Domain-Specific Languages with Xtext and Xtend, 2nd edn. Packt Publishing, Birmingham (2016)","edition":"2"},{"key":"23_CR5","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/0169-7552(87)90085-7","volume":"14","author":"T Bolognesi","year":"1987","unstructured":"Bolognesi, T., Brinksma, E.: Introduction to the ISO specification language LOTOS. Comput. Netw. 14, 25\u201359 (1987). https:\/\/doi.org\/10.1016\/0169-7552(87)90085-7","journal-title":"Comput. Netw."},{"issue":"3","key":"23_CR6","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/s10817-015-9358-9","volume":"56","author":"T Bourke","year":"2016","unstructured":"Bourke, T., van Glabbeek, R.J., H\u00f6fner, P.: Mechanizing a process algebra for network protocols. J. Autom. Reason. 56(3), 309\u2013341 (2016). https:\/\/doi.org\/10.1007\/s10817-015-9358-9","journal-title":"J. Autom. Reason."},{"key":"23_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/978-3-662-49498-1_5","volume-title":"Programming Languages and Systems","author":"E Bres","year":"2016","unstructured":"Bres, E., van Glabbeek, R., H\u00f6fner, P.: A timed process algebra for wireless networks with an application in routing. In: Thiemann, P. (ed.) ESOP 2016. LNCS, vol. 9632, pp. 95\u2013122. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49498-1_5"},{"key":"23_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-642-36742-7_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Cranen","year":"2013","unstructured":"Cranen, S., et al.: An overview of the mCRL2 toolset and its recent advances. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 199\u2013213. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_15"},{"issue":"3","key":"23_CR9","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1016\/0167-6423(83)90017-5","volume":"2","author":"EA Emerson","year":"1982","unstructured":"Emerson, E.A., Clarke, E.M.: Using branching time temporal logic to synthesize synchronization skeletons. Sci. Comput. Program. 2(3), 241\u2013266 (1982). https:\/\/doi.org\/10.1016\/0167-6423(83)90017-5","journal-title":"Sci. Comput. Program."},{"key":"23_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-642-28756-5_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Fehnker","year":"2012","unstructured":"Fehnker, A., van Glabbeek, R., H\u00f6fner, P., McIver, A., Portmann, M., Tan, W.L.: Automated analysis of AODV using UPPAAL. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 173\u2013187. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28756-5_13"},{"key":"23_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/978-3-642-28869-2_15","volume-title":"Programming Languages and Systems","author":"A Fehnker","year":"2012","unstructured":"Fehnker, A., van Glabbeek, R., H\u00f6fner, P., McIver, A., Portmann, M., Tan, W.L.: A process algebra for wireless mesh networks. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 295\u2013315. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28869-2_15"},{"key":"23_CR12","unstructured":"Fehnker, A., van Glabbeek, R.J., H\u00f6fner, P., McIver, A.K., Portmann, M., Tan, W.L.: A process algebra for wireless mesh networks used for modelling, verifying and analysing AODV (2013). http:\/\/arxiv.org\/abs\/1312.7645"},{"key":"23_CR13","series-title":"IFIP Advances in Information and Communication Technology","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-642-15240-5_3","volume-title":"Theoretical Computer Science","author":"RJ Glabbeek","year":"2010","unstructured":"Glabbeek, R.J.: The coarsest precongruences respecting safety and liveness properties. In: Calude, C.S., Sassone, V. (eds.) TCS 2010. IAICT, vol. 323, pp. 32\u201352. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15240-5_3"},{"key":"23_CR14","unstructured":"van Glabbeek, R.J.: Ensuring liveness properties of distributed systems (a research agenda). Position paper (2016). https:\/\/arxiv.org\/abs\/1711.04240"},{"key":"23_CR15","doi-asserted-by":"publisher","unstructured":"van Glabbeek, R.J., H\u00f6fner, P.: Split, send, reassemble: a formal specification of a CAN bus protocol stack. In: Hermanns, H., H\u00f6fner, P. (eds.) Models for formal analysis of real systems (MARS 2017), EPTCS, vol. 244, pp. 14\u201352. Open Publishing Association (2017). https:\/\/doi.org\/10.4204\/EPTCS.244.2","DOI":"10.4204\/EPTCS.244.2"},{"issue":"4","key":"23_CR16","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/s00446-015-0262-7","volume":"29","author":"RJ Glabbeek van","year":"2016","unstructured":"van Glabbeek, R.J., H\u00f6fner, P., Portmann, M., Tan, W.L.: Modelling and verifying the AODV routing protocol. Distrib. Comput. 29(4), 279\u2013315 (2016). https:\/\/doi.org\/10.1007\/s00446-015-0262-7","journal-title":"Distrib. Comput."},{"key":"23_CR17","doi-asserted-by":"crossref","unstructured":"van Glabbeek, R.J., H\u00f6fner, P., van der Wal, D.: Analysing AWN-specifications using mCRL2. Technical report, Data61, CSIRO (2018, to appear)","DOI":"10.1007\/978-3-319-98938-9_23"},{"key":"23_CR18","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/9946.001.0001","volume-title":"Modeling and Analysis of Communicating Systems","author":"JF Groote","year":"2014","unstructured":"Groote, J.F., Mousavi, M.R.: Modeling and Analysis of Communicating Systems. MIT Press, Cambridge (2014)"},{"issue":"1","key":"23_CR19","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1145\/2455.2460","volume":"32","author":"M Hennessy","year":"1985","unstructured":"Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J. ACM 32(1), 137\u2013161 (1985). https:\/\/doi.org\/10.1145\/2455.2460","journal-title":"J. ACM"},{"key":"23_CR20","volume-title":"Communicating Sequential Processes","author":"CAR Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall, Upper Saddle River (1985)"},{"issue":"12","key":"23_CR21","doi-asserted-by":"publisher","first-page":"2435","DOI":"10.1016\/j.scico.2012.11.009","volume":"78","author":"Y-L Hwong","year":"2013","unstructured":"Hwong, Y.-L., Keiren, J.A., Kusters, V.J.J., Leemans, S.J.J., Willemse, T.A.C.: Formalising and analysing the control software of the Compact Muon Solenoid Experiment at the Large Hadron Collider. Sci. Comput. Program. 78(12), 2435\u20132452 (2013). https:\/\/doi.org\/10.1016\/j.scico.2012.11.009","journal-title":"Sci. Comput. Program."},{"key":"23_CR22","unstructured":"IEEE: IEEE Standard for Information Technology\u2014Telecommunications and information exchange between systems\u2014Local and metropolitan area networks-Specific requirements Part 11: Wireless LAN Medium Access Control (MAC) and Physical Layer (PHY) specifications Amendment 10: Mesh Networking (2011). http:\/\/ieeexplore.ieee.org\/xpl\/articleDetails.jsp?arnumber=6018236"},{"key":"23_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"692","DOI":"10.1007\/978-3-662-46681-0_61","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Kant","year":"2015","unstructured":"Kant, G., Laarman, A., Meijer, J., van de Pol, J., Blom, S., van Dijk, T.: LTSmin: high-performance language-independent model checking. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 692\u2013707. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_61"},{"key":"23_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"286","DOI":"10.1007\/3-540-47884-1_16","volume-title":"Integrated Formal Methods","author":"S Kent","year":"2002","unstructured":"Kent, S.: Model driven engineering. In: Butler, M., Petre, L., Sere, K. (eds.) IFM 2002. LNCS, vol. 2335, pp. 286\u2013298. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-47884-1_16"},{"key":"23_CR25","unstructured":"Luttik, S.P.: Description and formal specification of the link layer of P1394. In: Lovrek, I. (ed.) 2nd International Workshop on Applied Formal Methods in System Design, pp. 43\u201356 (1997)"},{"key":"23_CR26","volume-title":"Communication and Concurrency","author":"R Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. Prentice Hall, Upper Saddle River (1989)"},{"key":"23_CR27","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-92293-3","volume-title":"QVT - Operational Mappings: Modellierung mit der Query Views Transformation","author":"S Nolte","year":"2010","unstructured":"Nolte, S.: QVT - Operational Mappings: Modellierung mit der Query Views Transformation. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-540-92293-3"},{"key":"23_CR28","unstructured":"Object Management Group: Meta Object Facility (MOF) 2.0 Query\/View\/ Transformation Specification (2011). http:\/\/www.omg.org\/spec\/QVT\/"},{"key":"23_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/BFb0017309","volume-title":"Theoretical Computer Science","author":"D Park","year":"1981","unstructured":"Park, D.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol. 104, pp. 167\u2013183. Springer, Heidelberg (1981). https:\/\/doi.org\/10.1007\/BFb0017309"},{"key":"23_CR30","unstructured":"Perkins, C.E., Belding-Royer, E.M., Das, S.: Ad hoc On-Demand Distance Vector (AODV) routing. RFC 3561 (Experimental), Network Working Group (2003). http:\/\/www.ietf.org\/rfc\/rfc3561.txt"},{"key":"23_CR31","doi-asserted-by":"publisher","unstructured":"Plotkin, G.D.: A structural approach to operational semantics. J. Log. Algebr. Program. 60\u201361, 17\u2013139 (2004). Originally appeared in 1981. https:\/\/doi.org\/10.1016\/j.jlap.2004.05.001","DOI":"10.1016\/j.jlap.2004.05.001"},{"key":"23_CR32","doi-asserted-by":"publisher","unstructured":"Pratt, V.R.: A Decidable mu-Calculus. In: Foundations of Computer Science (FOCS 1981), pp. 421\u2013427. IEEE Computer Society (1981). https:\/\/doi.org\/10.1109\/SFCS.1981.4","DOI":"10.1109\/SFCS.1981.4"},{"issue":"2","key":"23_CR33","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1109\/MC.2006.58","volume":"39","author":"DC Schmidt","year":"2006","unstructured":"Schmidt, D.C.: Model-driven engineering. Computer 39(2), 25\u201331 (2006). https:\/\/doi.org\/10.1109\/MC.2006.58","journal-title":"Computer"},{"key":"23_CR34","unstructured":"Soley, R., The OMG Staff Strategy Group: Model Driven Architecture (2000). http:\/\/www.omg.org\/~soley\/mda.html"},{"key":"23_CR35","volume-title":"EMF: Eclipse Modeling Framework 2.0","author":"D Steinberg","year":"2009","unstructured":"Steinberg, D., Budinsky, F., Paternostro, M., Merks, E.: EMF: Eclipse Modeling Framework 2.0, 2nd edn. Addison-Wesley, Boston (2009)","edition":"2"},{"key":"23_CR36","unstructured":"van der Wal, D.: Modeling AWN networks with an mCRL2 back end. Master\u2019s thesis, University of Twente (2018)"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-98938-9_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,21]],"date-time":"2019-10-21T21:02:08Z","timestamp":1571691728000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-98938-9_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319989372","9783319989389"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-98938-9_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}