{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,27]],"date-time":"2026-01-27T22:27:56Z","timestamp":1769552876908,"version":"3.49.0"},"reference-count":27,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014,10]]},"DOI":"10.1109\/healthcom.2014.7001811","type":"proceedings-article","created":{"date-parts":[[2015,1,13]],"date-time":"2015-01-13T15:14:46Z","timestamp":1421162086000},"page":"43-48","source":"Crossref","is-referenced-by-count":12,"title":["Formal reliability analysis of a typical FHIR standard based e-Health system using PRISM"],"prefix":"10.1109","author":[{"given":"Usman","family":"Pervez","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Osman","family":"Hasan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Khalid","family":"Latif","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sofiene","family":"Tahar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Amjad","family":"Gawanmeh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mohamed Salah","family":"Hamdi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"19","first-page":"429","article-title":"Ymer: A statistical model checker","author":"younes","year":"2005","journal-title":"International Conference on Computer Aided Verification 3576 of LNCS"},{"key":"17","doi-asserted-by":"publisher","DOI":"10.1145\/343369.343402"},{"key":"18","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2004.1459815"},{"key":"15","first-page":"585","article-title":"PRISM 4.0: Verification of probabilistic real-time systems","author":"kwiatkowska","year":"2011","journal-title":"International Conference on Computer Aided Verification 6806 of LNCS"},{"key":"16","doi-asserted-by":"publisher","DOI":"10.1016\/0377-2217(89)90348-2"},{"key":"13","doi-asserted-by":"publisher","DOI":"10.1145\/1368088.1368183"},{"key":"14","first-page":"41","article-title":"Formal model for e-healthcare readiness assessment in developing country context","author":"oio","year":"2007","journal-title":"International Conference on Innovations in Information Technology"},{"key":"11","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2006.113"},{"key":"12","doi-asserted-by":"publisher","DOI":"10.1109\/ICSM.2011.6081983"},{"key":"21","first-page":"251","article-title":"Vesta: A statistical model-checker and analyzer for probabilistic systems","author":"viswanathan","year":"2005","journal-title":"Second International Conference on the Quantitative Evaluation of Systems"},{"key":"20","first-page":"243","article-title":"A markov reward model checker","author":"khattri","year":"2005","journal-title":"Second International Conference on the Quantitative Evaluation of Systems"},{"key":"22","first-page":"673","article-title":"Etmcc: Model checking performability properties of markov chains","author":"meyer-kayser","year":"2003","journal-title":"International Conference on Dependable Systems and Networks"},{"key":"23","author":"fong","year":"2008","journal-title":"Method and System of Remote Diagnostic Control and Information Collection Using A Shared Resource"},{"key":"24","author":"berson","year":"1996","journal-title":"Client\/Server Architecture"},{"key":"25","author":"barry","year":"1999","journal-title":"Methods for Generating Patient-specific Medical Reports"},{"key":"26","year":"2014"},{"key":"27","first-page":"141","article-title":"An empirical transition matrix for non-homogeneous markov chains based on censored observations","volume":"5","author":"aalen","year":"1978","journal-title":"Scandinavian Journal of Statistics"},{"key":"3","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2009.283"},{"key":"2","year":"2014"},{"key":"10","doi-asserted-by":"publisher","DOI":"10.1109\/RBME.2012.2184750"},{"key":"1","year":"2014"},{"key":"7","doi-asserted-by":"publisher","DOI":"10.1007\/s11548-013-0919-2"},{"key":"6","doi-asserted-by":"publisher","DOI":"10.1007\/s10916-011-9739-5"},{"key":"5","first-page":"453","volume":"25","author":"hoogendoorn","year":"2009","journal-title":"Formal Verification of An Agent-based Support System for Medicine Intake"},{"key":"4","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1007\/978-3-642-32355-3_4","article-title":"Towards a formal integrated model of collaborative healthcare workflows","author":"bertolini","year":"2012","journal-title":"Foundations of Health Informatics Engineering and Systems"},{"key":"9","doi-asserted-by":"publisher","DOI":"10.1109\/CCNC.2013.6488581"},{"key":"8","first-page":"381","author":"benghazi","year":"2009","journal-title":"Applying Formal Verification Techniques to Ambient Assisted Living Systems 5872 of LNCS"}],"event":{"name":"2014 IEEE 16th International Conference on e-Health Networking, Applications and Services (Healthcom 2014)","location":"Natal","start":{"date-parts":[[2014,10,15]]},"end":{"date-parts":[[2014,10,18]]}},"container-title":["2014 IEEE 16th International Conference on e-Health Networking, Applications and Services (Healthcom)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/6992842\/7001800\/07001811.pdf?arnumber=7001811","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,22]],"date-time":"2017-06-22T23:34:54Z","timestamp":1498174494000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/7001811\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,10]]},"references-count":27,"URL":"https:\/\/doi.org\/10.1109\/healthcom.2014.7001811","relation":{},"subject":[],"published":{"date-parts":[[2014,10]]}}}