{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,5]],"date-time":"2025-04-05T22:05:38Z","timestamp":1743890738319},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319242545"},{"type":"electronic","value":"9783319242552"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-24255-2_4","type":"book-chapter","created":{"date-parts":[[2015,9,5]],"date-time":"2015-09-05T09:51:13Z","timestamp":1441446673000},"page":"29-43","source":"Crossref","is-referenced-by-count":8,"title":["The Formal Derivation of Mode Logic for Autonomous Satellite Flight Formation"],"prefix":"10.1007","author":[{"given":"Anton","family":"Tarasyuk","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Inna","family":"Pereverzeva","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Elena","family":"Troubitsyna","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Timo","family":"Latvala","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,11,25]]},"reference":[{"key":"4_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B","author":"JR Abrial","year":"2010","unstructured":"Abrial, J.R.: Modeling in Event-B. Cambridge University Press, Cambridge (2010)"},{"issue":"15","key":"4_CR2","doi-asserted-by":"publisher","first-page":"1263","DOI":"10.1016\/S1383-7621(98)00067-8","volume":"45","author":"GA Agha","year":"1999","unstructured":"Agha, G.A., Kim, W.: Actors: a unifying model for parallel and distributed computing. J. Syst. Archit. 45(15), 1263\u20131277 (1999)","journal-title":"J. Syst. Archit."},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"Buckreuss, S., Werninghaus, R., Pitz, W.: German satellite mission TerraSAR-X. In: Radar Conference 2008, pp. 1\u20135. IEEE (2008)","DOI":"10.1109\/RADAR.2008.4720788"},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"Castellanic, L.T., Llorente, S., Fernandez, J.M., Ruiz, M., Mestreau-Garreau, A., Cropp, A., Santovincenzo, A.: PROBA-3 mission. In: SFFMT 2013 (2013)","DOI":"10.1504\/IJSPACESE.2013.059268"},{"key":"4_CR5","unstructured":"Chaudemar, J.C., Bensana, E., Seguin, C.: Model based safety analysis for an unmanned aerial system. In: Dependable Robots in Human Environments (2010)"},{"key":"4_CR6","unstructured":"DEPLOY: IST FP7 IP Project. \n                      http:\/\/www.deploy-project.eu\/"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Esteve, M., Katoen, J., Nguyen, V.Y., Postma, B., Yushtein, Y.: Formal correctness, safety, dependability, and performance analysis of a satellite. In: ICSE 2012, pp. 1022\u20131031. IEEE (2012)","DOI":"10.1109\/ICSE.2012.6227118"},{"key":"4_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-642-11811-1_14","volume-title":"Abstract State Machines, Alloy, B and Z","author":"A Iliasov","year":"2010","unstructured":"Iliasov, A., Troubitsyna, E., Laibinis, L., Romanovsky, A., Varpaaniemi, K., Ilic, D., Latvala, T.: Supporting reuse in Event B development: modularisation approach. In: Frappier, M., Gl\u00e4sser, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) ABZ 2010. LNCS, vol. 5977, pp. 174\u2013188. Springer, Heidelberg (2010)"},{"key":"4_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-642-15651-9_10","volume-title":"Computer Safety, Reliability, and Security","author":"A Iliasov","year":"2010","unstructured":"Iliasov, A., Troubitsyna, E., Laibinis, L., Romanovsky, A., Varpaaniemi, K., V\u00e4is\u00e4nen, P., Ilic, D., Latvala, T.: Verifying mode consistency for on-board satellite software. In: Schoitsch, E. (ed.) SAFECOMP 2010. LNCS, vol. 6351, pp. 126\u2013141. Springer, Heidelberg (2010)"},{"issue":"7","key":"4_CR10","doi-asserted-by":"publisher","first-page":"884","DOI":"10.1016\/j.scico.2012.04.010","volume":"78","author":"A Iliasov","year":"2013","unstructured":"Iliasov, A., Troubitsyna, E., Laibinis, L., Romanovsky, A., Varpaaniemi, K., Ilic, D., Latvala, T.: Developing mode-rich satellite software by refinement in Event-B. Sci. Comput. Program. 78(7), 884\u2013905 (2013)","journal-title":"Sci. Comput. Program."},{"issue":"2","key":"4_CR11","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/s10009-007-0063-9","volume":"10","author":"M Leuschel","year":"2008","unstructured":"Leuschel, M., Butler, M.: ProB: an automated analysis toolset for the B method. Int. J. Softw. Tools Technol. Transf. 10(2), 185\u2013203 (2008)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"4_CR12","unstructured":"Leveson, N., Pinnel, L.D., Sandys, S.D., Koga, S., Reese, J.D.: Analyzing software specifications for mode confusion potential. In: Human Error and System Development, pp. 132\u2013146 (1997)"},{"key":"4_CR13","unstructured":"Peng, Z., Lu, Y., Miller, A., Zhao, T., Johnson, C.: Formal specification and quantitative analysis of a constellation of navigation satellites. CoRR abs\/1402.5599 (2014)"},{"key":"4_CR14","doi-asserted-by":"publisher","first-page":"296","DOI":"10.1016\/j.actaastro.2014.01.010","volume":"102","author":"TV Peters","year":"2014","unstructured":"Peters, T.V., Brancob, J., Escorial, D., Castellani, L.T., Cropp, A.: Mission analysis for PROBA-3 nominal operations. Acta Astronautica 102, 296\u2013310 (2014)","journal-title":"Acta Astronautica"},{"key":"4_CR15","unstructured":"Prisma Satellites. \n                      http:\/\/www.prismasatellites.se\/"},{"key":"4_CR16","unstructured":"Rodin: Modularisation plug-in. \n                      http:\/\/wiki.event-b.org\/index.php\/Modularisation_Plug-in"},{"key":"4_CR17","unstructured":"Rodin: Event-B platform. \n                      http:\/\/www.event-b.org\/"},{"key":"4_CR18","doi-asserted-by":"crossref","unstructured":"Rugina, A., Leorato, C., Tremolizzo, E.: Advanced validation of overall spacecraft behaviour concept using a collaborative modelling and simulation approach. In: WETICE 2012, pp. 262\u2013267. IEEE Computer Society (2012)","DOI":"10.1109\/WETICE.2012.37"},{"key":"4_CR19","unstructured":"Rugina, A.E., Blanquart, J.P., Soumagne, R.: Validating failure detection isolation and recovery strategies using timed automata. In: EWDC 2009 (2009)"},{"key":"4_CR20","doi-asserted-by":"crossref","unstructured":"Tarasyuk, A., Pereverzeva, I., Troubitsyna, E., Latvala, T.: The formal derivation of mode logic for autonomous satellite flight formation. Technical Report 1137, Turku Centre for Computer Science (2015)","DOI":"10.1007\/978-3-319-24255-2_4"},{"key":"4_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"210","DOI":"10.1007\/978-3-642-33678-2_18","volume-title":"Computer Safety, Reliability, and Security","author":"A Tarasyuk","year":"2012","unstructured":"Tarasyuk, A., Pereverzeva, I., Troubitsyna, E., Latvala, T., Nummila, L.: Formal development and assessment of a reconfigurable on-board satellite system. In: Ortmeier, F., Lipaczewski, M. (eds.) SAFECOMP 2012. LNCS, vol. 7612, pp. 210\u2013222. Springer, Heidelberg (2012)"},{"key":"4_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1007\/978-3-642-24270-0_17","volume-title":"Computer Safety, Reliability, and Security","author":"M Webster","year":"2011","unstructured":"Webster, M., Fisher, M., Cameron, N., Jump, M.: Formal methods for the certification of autonomous unmanned aircraft systems. In: Flammini, F., Bologna, S., Vittorini, V. (eds.) SAFECOMP 2011. LNCS, vol. 6894, pp. 228\u2013242. Springer, Heidelberg (2011)"}],"container-title":["Lecture Notes in Computer Science","Computer Safety, Reliability, and Security"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-24255-2_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T17:59:27Z","timestamp":1559239167000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-24255-2_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319242545","9783319242552"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-24255-2_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}