{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,15]],"date-time":"2025-11-15T03:57:17Z","timestamp":1763179037999,"version":"3.37.3"},"reference-count":49,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"1","license":[{"start":{"date-parts":[[2019,3,1]],"date-time":"2019-03-01T00:00:00Z","timestamp":1551398400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2019,3,1]],"date-time":"2019-03-01T00:00:00Z","timestamp":1551398400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2019,3,1]],"date-time":"2019-03-01T00:00:00Z","timestamp":1551398400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Systems Journal"],"published-print":{"date-parts":[[2019,3]]},"DOI":"10.1109\/jsyst.2018.2793665","type":"journal-article","created":{"date-parts":[[2018,2,6]],"date-time":"2018-02-06T19:17:45Z","timestamp":1517944665000},"page":"1018-1029","source":"Crossref","is-referenced-by-count":14,"title":["Model Checking Techniques Applied to Satellite Operational Mode Management"],"prefix":"10.1109","volume":"13","author":[{"given":"Vittoria","family":"Nardone","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2634-4456","authenticated-orcid":false,"given":"Antonella","family":"Santone","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4003-1613","authenticated-orcid":false,"given":"Massimo","family":"Tipaldi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1791-2295","authenticated-orcid":false,"given":"Davide","family":"Liuzza","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2753-1787","authenticated-orcid":false,"given":"Luigi","family":"Glielmo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1109\/AERO.2006.1656029"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1002\/j.2334-5837.2014.tb03142.x"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1002\/j.2334-5837.2017.00393.x"},{"key":"ref32","doi-asserted-by":"crossref","first-page":"256","DOI":"10.1016\/j.procs.2013.09.270","article-title":"Basis path analysis for testing complex system of systems","volume":"20","author":"zapata","year":"2013","journal-title":"Procedia Comput Sci"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1016\/j.procs.2013.09.276"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-89247-2_2"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1109\/ITSC.2015.71"},{"key":"ref36","first-page":"59","article-title":"Software engineering techniques for the development of Systems of Systems","author":"calinescu","year":"2008","journal-title":"Proc Monterey Workshop"},{"key":"ref35","doi-asserted-by":"crossref","first-page":"12","DOI":"10.1145\/2897829.2897833","article-title":"Modeling and verification for different types of system of systems using PRISM","author":"seo","year":"2016","journal-title":"Proc IEEE\/ACM 4th Int Workshop Softw Eng Syst Syst"},{"key":"ref34","volume":"24","author":"le?niewski","year":"2012","journal-title":"Lesniewski's Lecture Notes in Logic"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1109\/IMIS.2013.29"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2014.06.011"},{"article-title":"Language overview for PHAVer version 0.35","year":"2006","author":"frehse","key":"ref29"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1016\/j.actaastro.2015.04.018"},{"year":"2009","key":"ref1","article-title":"ECSS-E-ST-10C: Space Engineering - Systems Engineering General Requirements"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"ref22","first-page":"168","article-title":"Assume-guarantee model checking of software: A comparative case study","volume":"99","author":"pasareanu","year":"1999","journal-title":"Proc International SPIN Workshop on Model Checking of Software"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1145\/295558.295570"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.7146\/brics.v1i34.21609"},{"key":"ref23","first-page":"248","article-title":"Compositional model checking for linear-time temporal logic","author":"kaivola","year":"1992","journal-title":"Proc Int'l Workshop on Computer Aided Verification"},{"article-title":"META II: Formal co-verification of correctness of large-scale cyber-physical systems during design","year":"2011","author":"uckun","key":"ref26"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.3166\/ejc.18.217-238"},{"journal-title":"Communication and Concurrency","year":"1989","author":"milner","key":"ref10"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1109\/AERO.2013.6496878"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/44.1.21"},{"journal-title":"Principles of Model Checking","year":"2008","author":"baier","key":"ref12"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.1999.1660"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.2514\/1.I010307"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1016\/j.actaastro.2012.04.001"},{"key":"ref16","doi-asserted-by":"crossref","first-page":"573","DOI":"10.1007\/978-3-319-25150-9_33","article-title":"CAAL: concurrency workbench, aalborg edition","volume":"9399","author":"andersen","year":"2015","journal-title":"Theoretical Aspects of Computing—ICTAC 2015"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-005-1634-6"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-005-4591-1"},{"key":"ref19","first-page":"419","article-title":"Symbolic model checking","author":"clarke","year":"1996","journal-title":"Proc 8th Comput Aided Verif Conf"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1016\/j.actaastro.2015.02.009"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1109\/SYSOSE.2015.7151937"},{"key":"ref6","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-25170-2","author":"eickhoff","year":"2012","journal-title":"Onboard Computers Onboard Software and Satellite Operations-an Introduction"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1016\/j.ress.2014.07.003"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1145\/2591062.2591183"},{"key":"ref49","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2013.03.005"},{"journal-title":"Model checking","year":"2001","author":"clarke","key":"ref7"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2012.6227118"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1109\/ACC.2012.6315141"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.2514\/6.2011-1506"},{"year":"2009","key":"ref48","article-title":"ECSS-E-ST-40C: Space Engineering—Software."},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1109\/ACC.2014.6859229"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2013.2295764"},{"key":"ref41","first-page":"1","article-title":"Formal verification in early mission planning","author":"fischer","year":"2012","journal-title":"Proc SESP Simul EGSE facilities"},{"key":"ref44","first-page":"13","article-title":"Behavioral modeling and run-time verification of system-of-systems architectural requirements","author":"drusinsky","year":"2004","journal-title":"Int Conf Comput Commun Contr Tech"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1002\/sys.20095"}],"container-title":["IEEE Systems Journal"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/4267003\/8649702\/08283556.pdf?arnumber=8283556","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,13]],"date-time":"2022-07-13T21:04:08Z","timestamp":1657746248000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/8283556\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,3]]},"references-count":49,"journal-issue":{"issue":"1"},"URL":"https:\/\/doi.org\/10.1109\/jsyst.2018.2793665","relation":{},"ISSN":["1932-8184","1937-9234","2373-7816"],"issn-type":[{"type":"print","value":"1932-8184"},{"type":"electronic","value":"1937-9234"},{"type":"electronic","value":"2373-7816"}],"subject":[],"published":{"date-parts":[[2019,3]]}}}