{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T15:14:19Z","timestamp":1743088459156,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642331695"},{"type":"electronic","value":"9783642331701"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-33170-1_5","type":"book-chapter","created":{"date-parts":[[2013,7,9]],"date-time":"2013-07-09T08:56:29Z","timestamp":1373360189000},"page":"45-62","source":"Crossref","is-referenced-by-count":1,"title":["Deployment in the Space Sector"],"prefix":"10.1007","author":[{"given":"Dubravka","family":"Ili\u0107","sequence":"first","affiliation":[]},{"given":"Linas","family":"Laibinis","sequence":"additional","affiliation":[]},{"given":"Timo","family":"Latvala","sequence":"additional","affiliation":[]},{"given":"Elena","family":"Troubitsyna","sequence":"additional","affiliation":[]},{"given":"Kimmo","family":"Varpaaniemi","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"5_CR1","unstructured":"DEPLOY. Deliverable D20 D3.1\u2014Report on pilot deployment in the space sector (January 2010)"},{"key":"5_CR2","unstructured":"DEPLOY. Deliverable D39 D3.2\u2014Report on enhanced deployment in the space sector (August 2011)"},{"key":"5_CR3","unstructured":"DEPLOY. Deliverable D5 JD1: Report on knowledge transfer (January 2009)"},{"key":"5_CR4","unstructured":"ESA. ECSS-E-70-41A: Space engineering: Ground systems and operations\u2014Telemetry and telecommand packet utilisation. European Space Agency Requirements and Standards Division, Noordwijk ZH, The Netherlands (January 2003). http:\/\/www.ecss.nl\/"},{"key":"5_CR5","unstructured":"ESA. ECSS-E-ST-40C: Space engineering\u2014Software. European Space Agency Requirements and Standards Division, Noordwijk ZH, The Netherlands (March 2009)"},{"key":"5_CR6","unstructured":"ESA. ECSS-Q-ST-80C: Space product assurance\u2014Software product assurance. European Space Agency Requirements and Standards Division, Noordwijk ZH, The Netherlands (March 2009)"},{"key":"5_CR7","unstructured":"ESA. Factsheet: BepiColombo (February 2012). http:\/\/www.esa.int\/esaSC\/SEMNEM3MDAF"},{"key":"5_CR8","unstructured":"Event-B. Documentation wiki: Rodin plug-ins (February 2012)"},{"key":"5_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"328","DOI":"10.1007\/978-3-642-20398-5_24","volume-title":"NASA Formal Methods, Proceedings","author":"A.S. Fathabadi","year":"2011","unstructured":"Fathabadi, A.S., Rezazadeh, R., Butler, M.J.: Applying atomicity and model decomposition to a space craft system in Event-B. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NASA Formal Methods, Proceedings, Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18\u201320, 2011. Lecture Notes in Computer Science, vol. 6617, pp.\u00a0328\u2013342. Springer, Berlin (2011)"},{"key":"5_CR10","unstructured":"Fathabadi, A.S., Rezazadeh, R., Butler, M.J.: Event-B project BepiColombo_Soton_v18.0 (Rodin archive of space system) (October 2010). http:\/\/eprints.ecs.soton.ac.uk\/22048\/"},{"key":"5_CR11","unstructured":"Iliasov, A., Laibinis, L., Troubitsyna, E.: An Event-B model of the attitude and orbit control system (March 2010). http:\/\/deploy-eprints.ecs.soton.ac.uk\/213\/"},{"key":"5_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"420","DOI":"10.1007\/978-3-642-24559-6_29","volume-title":"Formal Methods and Software Engineering, Proceedings","author":"A. Iliasov","year":"2011","unstructured":"Iliasov, A., Laibinis, L., Troubitsyna, E., Romanovsky, A.: Formal derivation of a distributed program in Event B. In: Qin, S., Qiu, Z. (eds.) Formal Methods and Software Engineering, Proceedings, 13th International Conference on Formal Engineering Methods, ICFEM 2011, Durham, UK, October 26\u201328, 2011. Lecture Notes in Computer Science, vol. 6991, pp. 420\u2013436. Springer, Berlin (2011)"},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"Iliasov, A., Laibinis, L., Troubitsyna, E., Romanovsky, A., Latvala, T.: Augmenting Event\u00a0B modelling with real-time verification. Technical report 1006, Turku Centre for Computer Science, Turku, Finland (April 2011)","DOI":"10.1109\/FormSERA.2012.6229789"},{"key":"5_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1007\/978-3-642-15898-8_4","volume-title":"Formal Methods for Industrial Critical Systems, Proceedings","author":"A. Iliasov","year":"2010","unstructured":"Iliasov, A., Troubitsyna, E., Laibinis, L., Romanovsky, A., Varpaaniemi, K., Ili\u0107, D., Latvala,\u00a0T.: Developing mode-rich satellite software by refinement in Event B. In: Kowalewski,\u00a0S., Roveri, M. (eds.) Formal Methods for Industrial Critical Systems, Proceedings, 15th International Workshop, FMICS 2010, Antwerp, Belgium, September 20\u201321, 2010. Lecture Notes in Computer Science, vol. 6371, pp. 50\u201366. Springer, Berlin (2010)"},{"key":"5_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"126","DOI":"10.1007\/978-3-642-15651-9_10","volume-title":"Computer Safety, Reliability, and Security: 29th International Conference, Proceedings","author":"A. Iliasov","year":"2010","unstructured":"Iliasov, A., Troubitsyna, E., Laibinis, L., Romanovsky, A., Varpaaniemi, K., V\u00e4is\u00e4nen, P., Ili\u0107,\u00a0D., Latvala, T.: Verifying mode consistency for on-board satellite software. In: Schoitsch,\u00a0E. (ed.) Computer Safety, Reliability, and Security: 29th International Conference, Proceedings, SAFECOMP 2010, Vienna, Austria, September 14\u201317, 2010. Lecture Notes in Computer Science, vol. 6351, pp. 126\u2013141. Springer, Berlin (2010)"},{"key":"5_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"174","DOI":"10.1007\/978-3-642-11811-1_14","volume-title":"Abstract State Machines, Alloy, B and\u00a0Z: Second International Conference, Proceedings","author":"I. Iliasov","year":"2010","unstructured":"Iliasov, I., Troubitsyna, E., Laibinis, L., Romanovsky, A., Varpaaniemi, K., Ili\u0107, D., Latvala,\u00a0T.: Supporting reuse in Event B development: Modularisation approach. In: Frappier,\u00a0M., Gl\u00e4sser, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) Abstract State Machines, Alloy, B and\u00a0Z: Second International Conference, Proceedings, ABZ 2010, Orford, Qu\u00e9bec, Canada, February 22\u201325, 2010. Lecture Notes in Computer Science, vol. 5977, pp. 174\u2013188. Springer, Berlin (2010)"},{"key":"5_CR17","unstructured":"Ili\u0107, D., Varpaaniemi, K.: Event-B project BepiColombo_Models_v5.0 (May 2009). http:\/\/deploy-eprints.ecs.soton.ac.uk\/136\/"},{"key":"5_CR18","first-page":"180","volume-title":"Proceedings of the 22nd IEEE International Symposium on Software Reliability Engineering","author":"I. Lopatkin","year":"2011","unstructured":"Lopatkin, I., Iliasov, A., Romanovsky, A.: Rigorous development of dependable systems using fault tolerance views. In: Dohi, T., \u010cuki\u0107, B. (eds.) Proceedings of the 22nd IEEE International Symposium on Software Reliability Engineering, ISSRE 2011, Hiroshima, Japan, November\u00a029\u2013December 2, 2011, pp. 180\u2013189. IEEE Computer Society Press, Los Alamitos (2011)"},{"key":"5_CR19","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1109\/HASE.2011.10","volume-title":"Proceedings of the 2011 IEEE 13th International Symposium on High-Assurance Systems Engineering","author":"I. Lopatkin","year":"2011","unstructured":"Lopatkin, I., Iliasov, A., Romanovsky, A., Prokhorova, Y., Troubitsyna, E.: Patterns for representing FMEA in formal specification of control systems. In: Agarwal, A., Gokhale, S., Khosoftaar, T.M. (eds.) Proceedings of the 2011 IEEE 13th International Symposium on High-Assurance Systems Engineering, HASE 2011, Boca Raton, FL, USA, November 10\u201312, 2011, pp. 146\u2013151. IEEE Computer Society Press, Los Alamitos (2011)"},{"key":"5_CR20","unstructured":"NuSMV. A new symbolic model checker (February 2012). http:\/\/nusmv.fbk.eu\/"},{"key":"5_CR21","unstructured":"ProB. Animator and model checker (February 2012). http:\/\/www.stups.uni-duesseldorf.de\/ProB\/index.php5\/Main"},{"key":"5_CR22","first-page":"49","volume-title":"Proceedings of the 18th Asia-Pacific Software Engineering Conference","author":"Y. Prokhorova","year":"2011","unstructured":"Prokhorova, Y., Laibinis, L., Troubitsyna, E., Varpaaniemi, K., Latvala, T.: Derivation and formal verification of a mode logic for layered control systems. In: Thu, T.D., Leung, K.R.P.H. (eds.) Proceedings of the 18th Asia-Pacific Software Engineering Conference, APSEC 2011, Ho Chi Minh City, Vietnam, December 5\u20138, 2011, pp. 49\u201356. IEEE Computer Society Press, Los Alamitos (2011)"},{"key":"5_CR23","unstructured":"R\u00e4s\u00e4nen, T., Nummila, L.: DEPLOY training evaluation document (September 2010). http:\/\/deploy-eprints.ecs.soton.ac.uk\/314\/"},{"key":"5_CR24","unstructured":"RTCA. DO-178B: Software Considerations in airborne systems and equipment certification. Radio Technical Commission for Aeronautics, Washington, DC, USA (January 1992)"},{"key":"5_CR25","unstructured":"UPPAAL. An integrated tool environment for modelling, validation and verification of real-time systems (February 2012)"},{"key":"5_CR26","unstructured":"V\u00e4is\u00e4nen, P., Varpaaniemi, K.: DEPLOY satellite (an attitude and orbit control system) specification, version 15 (January 2010). http:\/\/deploy-eprints.ecs.soton.ac.uk\/167\/"},{"key":"5_CR27","unstructured":"Varpaaniemi, K.: DEPLOY work package 3 attitude and orbit control system software requirements document, DEP-RP-SSF-R-005, issue 1.0 (December 2010). http:\/\/deploy-eprints.ecs.soton.ac.uk\/266\/"},{"key":"5_CR28","unstructured":"Varpaaniemi, K.: DEPLOY work package 3 software requirements document for a distributed system for attitude and orbit control for a single spacecraft, DEP-RP-SSF-R-006, issue 1.3. (October 2011)"},{"key":"5_CR29","unstructured":"Varpaaniemi, K.: Event-B project BepiColombo_Models_v6.4 (September 2010). http:\/\/deploy-eprints.ecs.soton.ac.uk\/244\/"},{"key":"5_CR30","unstructured":"Varpaaniemi, K.: Event-B project DepSatSpec015Model000 (January 2010). http:\/\/deploy-eprints.ecs.soton.ac.uk\/168\/"},{"key":"5_CR31","unstructured":"Varpaaniemi, K.: Event-B projects DSAOCSSv002 and DSAOCSSv003 with special files for ProB Classic (October 2011). http:\/\/deploy-eprints.ecs.soton.ac.uk\/331\/"},{"key":"5_CR32","unstructured":"Varpaaniemi, K.: Some NuSMV experiments on the mode synchronization protocol in DSAOCSS (January 2012). http:\/\/deploy-eprints.ecs.soton.ac.uk\/362\/"}],"container-title":["Industrial Deployment of System Engineering Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-33170-1_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,19]],"date-time":"2023-02-19T12:23:35Z","timestamp":1676809415000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-642-33170-1_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642331695","9783642331701"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-33170-1_5","relation":{},"subject":[],"published":{"date-parts":[[2013]]}}}