{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,4]],"date-time":"2026-04-04T10:53:03Z","timestamp":1775299983736,"version":"3.50.1"},"reference-count":34,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/OAPA.html"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Access"],"published-print":{"date-parts":[[2018]]},"DOI":"10.1109\/access.2018.2885249","type":"journal-article","created":{"date-parts":[[2018,12,6]],"date-time":"2018-12-06T19:07:13Z","timestamp":1544123233000},"page":"78766-78779","source":"Crossref","is-referenced-by-count":5,"title":["Discrete-Time Systems Modeling and Verification With Alvis Language and Tools"],"prefix":"10.1109","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4925-3271","authenticated-orcid":false,"given":"Marcin","family":"Szpyrka","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michal","family":"Wypych","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jerzy","family":"Biernacki","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lukasz","family":"Podolski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-012-0177-x"},{"key":"ref32","doi-asserted-by":"crossref","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","article-title":"PRISM 4.0: Verification of probabilistic real-time systems","volume":"6806","author":"kwiatkowska","year":"2011","journal-title":"Proc 23rd Int Conf Comput Aided Verification (CAV)"},{"key":"ref31","author":"harel","year":"1998","journal-title":"Modeling Reactive Systems with Statecharts The STATEMATE Approach"},{"key":"ref30","article-title":"Real-time statechart semantics","author":"giese","year":"2003"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2016.2597061"},{"key":"ref10","first-page":"1607","article-title":"Alvis language with time dependence","author":"szpyrka","year":"2013","journal-title":"Proc Fed Conf Comput Sci Inf Syst"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1109\/MIXDES.2016.7529784"},{"key":"ref12","first-page":"161","article-title":"Formal description of Alvis language with $\\alpha^{0}$ system layer","volume":"129","author":"szpyrka","year":"2014","journal-title":"Fund Inform"},{"key":"ref13","author":"o\u2019sullivan","year":"2008","journal-title":"Real World Haskell"},{"key":"ref14","doi-asserted-by":"crossref","first-page":"334","DOI":"10.1007\/978-3-319-08867-9_22","article-title":"The nuXmv symbolic model checker","volume":"8559","author":"cavada","year":"2014","journal-title":"Computer Aided Verification"},{"key":"ref15","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1007\/s10009-012-0244-z","article-title":"CADP 2011: A toolbox for the construction and analysis of distributed processes","volume":"15","author":"garavel","year":"2013","journal-title":"Int J Softw Tools Technol Transf"},{"key":"ref16","author":"baier","year":"2008","journal-title":"Principles of Model Checking"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1090\/dimacs\/031\/06"},{"key":"ref18","author":"clarke","year":"1999","journal-title":"Model checking"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050046"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90035-9"},{"key":"ref4","author":"bergstra","year":"2001","journal-title":"Handbook of Process Algebra"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33278-4"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-59060-8_54"},{"key":"ref29","first-page":"591","article-title":"Timed and hybrid statecharts and their textual representation","author":"kesten","year":"1991","journal-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems"},{"key":"ref5","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1007\/978-3-540-27755-2_3","article-title":"Timed automata: Semantics, algorithms and tools","volume":"3098","author":"bengtsson","year":"2004","journal-title":"Lectures on Concurrency and Petri Nets"},{"key":"ref8","first-page":"55","article-title":"Hierarchical communication diagrams","volume":"35","author":"szpyrka","year":"2016","journal-title":"Inform Comput"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-65208-5_12"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1007\/b95112"},{"key":"ref9","author":"szpyrka","year":"2017","journal-title":"Alvis Modelling Language"},{"key":"ref1","doi-asserted-by":"crossref","first-page":"315","DOI":"10.1007\/978-3-642-21271-0_15","article-title":"Alvis—Modelling language for concurrent systems","volume":"362","author":"szpyrka","year":"2011","journal-title":"Intelligent Decision Systems in Large-Scale Distributed Environments"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.15439\/2016F264"},{"key":"ref22","author":"lee","year":"2012","journal-title":"Advances in GLIM and Statistical Modelling"},{"key":"ref21","author":"idris","year":"2014","journal-title":"Python for data analysis"},{"key":"ref24","author":"gorowski","year":"2014","journal-title":"Rail Transportation"},{"key":"ref23","year":"2015","journal-title":"Infrared System"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-007-0038-x"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1109\/5.24143"}],"container-title":["IEEE Access"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/6287639\/8274985\/08565865.pdf?arnumber=8565865","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,4]],"date-time":"2026-04-04T09:55:00Z","timestamp":1775296500000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/8565865\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"references-count":34,"URL":"https:\/\/doi.org\/10.1109\/access.2018.2885249","relation":{},"ISSN":["2169-3536"],"issn-type":[{"value":"2169-3536","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}