{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,13]],"date-time":"2024-09-13T09:54:52Z","timestamp":1726221292350},"reference-count":25,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2018,12,1]],"date-time":"2018-12-01T00:00:00Z","timestamp":1543622400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Innovations Syst Softw Eng"],"published-print":{"date-parts":[[2018,12]]},"DOI":"10.1007\/s11334-018-0318-5","type":"journal-article","created":{"date-parts":[[2018,12,22]],"date-time":"2018-12-22T08:10:00Z","timestamp":1545466200000},"page":"245-262","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Formal verification of SysML diagram using case studies of real-time system"],"prefix":"10.1007","volume":"14","author":[{"given":"Sajjad","family":"Ali","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,12,22]]},"reference":[{"key":"318_CR1","volume-title":"Principles of model checking","author":"C Baier","year":"2008","unstructured":"Baier C, Katoen J-P (2008) Principles of model checking, vol 26202649. MIT press, Cambridge"},{"key":"318_CR2","unstructured":"OMG Systems Modeling Language (OMG SysML). \n                    http:\/\/www.omg.org\/spec\/SysML\/1.3\/\n                    \n                   (June, 2012)"},{"key":"318_CR3","unstructured":"OMG Unified Modeling Language (OMG UML). \n                    http:\/\/www.omg.org\/spec\/UML\/2.4.1\/\n                    \n                   (August, 2011)"},{"key":"318_CR4","doi-asserted-by":"crossref","unstructured":"Jarraya Y, Soeanu A, Debbabi M, Hassaine F (2007). Automatic verification and performance analysis of time-constrained sysml activity diagrams. In: 14th annual IEEE international conference and workshops on the engineering of computer-based systems, 2007. ECBS \u201907, IEEE pp 515\u2013522","DOI":"10.1109\/ECBS.2007.22"},{"key":"318_CR5","volume-title":"Model checking","author":"EM Clarke","year":"1999","unstructured":"Clarke EM, Grumberg O, Peled D (1999) Model checking. MIT Press, Cambridge"},{"key":"318_CR6","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/0-8176-4404-0_21","volume-title":"Handbook of networked and embedded control systems","author":"JF Raskin","year":"2005","unstructured":"Raskin JF (2005) An introduction to hybrid automata. In: Johansson K, T\u00f6rngren M, Nielsen L (eds) Handbook of networked and embedded control systems. Birkhauser, Boston, pp 491\u2013517"},{"key":"318_CR7","doi-asserted-by":"crossref","unstructured":"Ouchani S, Mohamed OA, Debbabi M (2013) A probabilistic verification framework of SysML activity diagrams. In: 2013 IEEE 12th international conference on intelligent software methodologies, tools and techniques (SoMeT). IEEE, pp 165\u2013170","DOI":"10.1109\/SoMeT.2013.6645657"},{"issue":"6","key":"318_CR8","doi-asserted-by":"publisher","first-page":"2713","DOI":"10.1016\/j.eswa.2013.10.064","volume":"41","author":"S Ouchani","year":"2014","unstructured":"Ouchani S, Mohamed OA, Debbabi M (2014) A formal verification framework for sysml activity diagrams. Expert Syst Appl 41(6):2713\u20132728","journal-title":"Expert Syst Appl"},{"key":"318_CR9","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1016\/j.knosys.2013.11.016","volume":"56","author":"S Ouchani","year":"2014","unstructured":"Ouchani S, Mohamed OA, Debbabi M (2014) A property-based abstraction framework for sysml activity diagrams. Knowl Based Syst 56:328\u2013343","journal-title":"Knowl Based Syst"},{"key":"318_CR10","doi-asserted-by":"crossref","unstructured":"Ouchani S, Mohamed OA, Debbabi M (2012) Efficient probabilistic abstraction for SysML activity diagrams. In: Software engineering and formal methods. Springer, Berlin, pp 263\u2013277","DOI":"10.1007\/978-3-642-33826-7_18"},{"key":"318_CR11","doi-asserted-by":"crossref","unstructured":"Jarraya Y, Debbabi M, Bentahar J (2009). On the meaning of SysML activity diagrams. In: ECBS 2009, 16th annual IEEE international conference and workshop on the engineering of computer based systems, 2009. IEEE, pp 95\u2013105","DOI":"10.1109\/ECBS.2009.25"},{"key":"318_CR12","doi-asserted-by":"crossref","unstructured":"Debbabi M, Hassaine F, Jarraya Y, Soeanu A, Alawneh L (2010) Probabilistic model checking of SysML activity diagrams. In: Verification and validation in systems engineering. Springer, Berlin, pp 153\u2013166","DOI":"10.1007\/978-3-642-15228-3_9"},{"key":"318_CR13","doi-asserted-by":"crossref","unstructured":"Jansen DN, Hermanns H, Katoen JP (2002) A probabilistic extension of UML statecharts. In: Formal techniques in real-time and fault-tolerant systems. Springer, Berlin, pp 355\u2013374","DOI":"10.1007\/3-540-45739-9_21"},{"key":"318_CR14","unstructured":"Bianco VD, Lavazza L, Mauri M (December 2002) Model checking UML specifications of real time software. In: Eighth IEEE international conference on engineering of complex computer systems, 2002. Proceedings. IEEE, pp 203\u2013212"},{"key":"318_CR15","doi-asserted-by":"crossref","unstructured":"Basit-Ur-Rahim MA, Arif F, Ahmad J ( January 2014) Formal verification of sequence diagram using divine. In: 2014 World Congress on computer applications and information systems (WCCAIS). IEEE, pp 1\u20136","DOI":"10.1109\/WCCAIS.2014.6916659"},{"key":"318_CR16","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1016\/j.entcs.2009.09.064","volume":"254","author":"V Lima","year":"2009","unstructured":"Lima V, Talhi C, Mouheb D, Debbabi M, Wang L, Pourzandi M (2009) Formal verification and validation of UML 2.0 sequence diagrams using source and destination of messages. Electron Notes Theor Comput Sci 254:143\u2013160","journal-title":"Electron Notes Theor Comput Sci"},{"key":"318_CR17","unstructured":"Mazzini S, Puri S, Mari F, Melatti I, Tronci E\u00a0(2009) Formal verification at system level, DAta Systems in Aerospace (DASIA), Org. EuroSpace, Canadian Space Agency, CNES, ESA, EUMETSAT, Instanbul, Turkey"},{"issue":"1","key":"318_CR18","first-page":"1653","volume":"14","author":"D Soliman","year":"2012","unstructured":"Soliman D, Thramboulidis K, Frey G (2012) Function block diagram to uppaal timed automata transformation based on formal models. Inf Control Probl Manuf 14(1):1653\u20131659","journal-title":"Inf Control Probl Manuf"},{"key":"318_CR19","doi-asserted-by":"crossref","unstructured":"Linhares MV, Oliveira RSD, Farines JM, Vernadat F (September 2007) Introducing the modeling and verification process in SysML. In: Emerging technologies and factory automation. IEEE Conference on ETFA 2007. IEEE, pp 344\u2013351","DOI":"10.1109\/EFTA.2007.4416788"},{"key":"318_CR20","doi-asserted-by":"crossref","unstructured":"Ali S, Basit-Ur-Rahim MA, Arif F (June 2015) Formal verification of internal block diagram of SysML for modeling real-time system. In: 16th IEEE\/ACIS international conference on software engineering, artificial intelligence, networking and parallel\/distributed computing (SNPD 2015). IEEE (in press)","DOI":"10.1109\/SNPD.2015.7176271"},{"key":"318_CR21","doi-asserted-by":"crossref","unstructured":"Ali S, Basit-Ur-Rahim MA, Arif F (June 2015) Formal verification of time constrains SysML internal block diagram using prism. In: 15th international conference on computational science and its applications (ICCSA 2015). IEEE (in press)","DOI":"10.1109\/ICCSA.2015.11"},{"key":"318_CR22","doi-asserted-by":"crossref","unstructured":"Hinton A, Kwiatkowska M, Norma G, Parker D (2006) Prism: a tool for automatic verification of probabilistic systems. In: Tools and algorithms for the construction and analysis of systems. Springer, Berlin, pp 441\u2013444","DOI":"10.1007\/11691372_29"},{"key":"318_CR23","doi-asserted-by":"crossref","unstructured":"Clarke E, Grumberg O, Jha S, Lu Y, Veith H (2000) Counterexample-guided abstraction refinement. In: Computer aided verification. Springer, Berlin, pp 154\u2013169","DOI":"10.1007\/10722167_15"},{"issue":"4","key":"318_CR24","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1145\/2528935","volume":"14","author":"T Chen","year":"2013","unstructured":"Chen T, Diciolla M, Kwiatkowska M, Mereacre A (2013) Verification of linear duration properties over continuous-time markov chains. ACM Trans Comput Logic: TOCL 14(4):33","journal-title":"ACM Trans Comput Logic: TOCL"},{"key":"318_CR25","doi-asserted-by":"crossref","unstructured":"Kwiatkowska M, Norman G, Parker D (2007) Stochastic model checking. In: Formal methods for performance evaluation. Springer, Berlin, pp 220\u2013270","DOI":"10.1007\/978-3-540-72522-0_6"}],"container-title":["Innovations in Systems and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11334-018-0318-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-018-0318-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-018-0318-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,12,22]],"date-time":"2019-12-22T00:03:50Z","timestamp":1576973030000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11334-018-0318-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,12]]},"references-count":25,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2018,12]]}},"alternative-id":["318"],"URL":"https:\/\/doi.org\/10.1007\/s11334-018-0318-5","relation":{},"ISSN":["1614-5046","1614-5054"],"issn-type":[{"value":"1614-5046","type":"print"},{"value":"1614-5054","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,12]]},"assertion":[{"value":"3 August 2017","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"6 December 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"22 December 2018","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}