{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,18]],"date-time":"2026-03-18T14:20:52Z","timestamp":1773843652265,"version":"3.50.1"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319576657","type":"print"},{"value":"9783319576664","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-57666-4_16","type":"book-chapter","created":{"date-parts":[[2017,4,12]],"date-time":"2017-04-12T08:18:42Z","timestamp":1491985122000},"page":"260-279","source":"Crossref","is-referenced-by-count":17,"title":["Architecture-Based Design: A Satellite On-Board Software Case Study"],"prefix":"10.1007","author":[{"given":"Anastasia","family":"Mavridou","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Emmanouela","family":"Stachtiari","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Simon","family":"Bliudze","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anton","family":"Ivanov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Panagiotis","family":"Katsaros","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joseph","family":"Sifakis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,4,13]]},"reference":[{"issue":"3","key":"16_CR1","doi-asserted-by":"crossref","first-page":"329","DOI":"10.1017\/S0960129504004153","volume":"14","author":"F Arbab","year":"2004","unstructured":"Arbab, F.: Reo: a channel-based coordination model for component composition. Math. Struct. Comput. Sci. 14(3), 329\u2013366 (2004)","journal-title":"Math. Struct. Comput. Sci."},{"issue":"2","key":"16_CR2","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1007\/s00165-015-0349-8","volume":"18","author":"P Attie","year":"2016","unstructured":"Attie, P., et al.: A general framework for architecture composability. Formal Aspects Comput. 18(2), 207\u2013231 (2016)","journal-title":"Formal Aspects Comput."},{"key":"16_CR3","series-title":"Representation and Mind Series","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. Representation and Mind Series. The MIT Press, Cambridge (2008)"},{"key":"16_CR4","series-title":"SEI Series in Software Engineering","volume-title":"Software Architecture in Practice","author":"L Bass","year":"2012","unstructured":"Bass, L., Clements, P., Kazman, R.: Software Architecture in Practice. SEI Series in Software Engineering, 3rd edn. Addison-Wesley Professional, New York (2012)","edition":"3"},{"key":"16_CR5","unstructured":"Basu, A., et al.: Incremental component-based construction and verification of a robotic system. In: ECAI, pp. 631\u2013635. IOS Press (2008)"},{"issue":"3","key":"16_CR6","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1109\/MS.2011.27","volume":"28","author":"A Basu","year":"2011","unstructured":"Basu, A., et al.: Rigorous component-based system design using the BIP framework. IEEE Softw. 28(3), 41\u201348 (2011)","journal-title":"IEEE Softw."},{"key":"16_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1007\/978-3-642-20398-5_32","volume-title":"NASA Formal Methods","author":"S Bensalem","year":"2011","unstructured":"Bensalem, S., Griesmayer, A., Legay, A., Nguyen, T.-H., Sifakis, J., Yan, R.: D-Finder 2: towards efficient correctness of incremental design. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 453\u2013458. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-20398-5_32"},{"key":"16_CR8","unstructured":"Benveniste, A., et al.: Contracts for system design. Research report RR-8147, INRIA, November 2012"},{"issue":"10","key":"16_CR9","doi-asserted-by":"crossref","first-page":"1315","DOI":"10.1109\/TC.2008.26","volume":"57","author":"S Bliudze","year":"2008","unstructured":"Bliudze, S., Sifakis, J.: The algebra of connectors-structuring interaction in BIP. IEEE Trans. Comput. 57(10), 1315\u20131330 (2008)","journal-title":"IEEE Trans. Comput."},{"key":"16_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-319-24953-7_25","volume-title":"Automated Technology for Verification and Analysis","author":"S Bliudze","year":"2015","unstructured":"Bliudze, S., Cimatti, A., Jaber, M., Mover, S., Roveri, M., Saab, W., Wang, Q.: Formal verification of infinite-state BIP models. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) ATVA 2015. LNCS, vol. 9364, pp. 326\u2013343. Springer, Cham (2015). doi: 10.1007\/978-3-319-24953-7_25"},{"key":"16_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1007\/978-3-642-14295-6_37","volume-title":"Computer Aided Verification","author":"R Bloem","year":"2010","unstructured":"Bloem, R., Cimatti, A., Greimel, K., Hofferek, G., K\u00f6nighofer, R., Roveri, M., Schuppan, V., Seeber, R.: RATSY \u2013 a new requirements analysis tool with synthesis. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 425\u2013429. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-14295-6_37"},{"key":"16_CR12","volume-title":"SCADE: Language and Applications","author":"J-L Boulanger","year":"2015","unstructured":"Boulanger, J.-L., et al.: SCADE: Language and Applications, 1st edn. Wiley-IEEE Press, New York (2015)","edition":"1"},{"key":"16_CR13","doi-asserted-by":"crossref","first-page":"20","DOI":"10.1016\/j.ress.2014.07.003","volume":"132","author":"M Bozzano","year":"2014","unstructured":"Bozzano, M., et al.: Spacecraft early design validation using formal methods. Reliab. Eng. Syst. Saf. 132, 20\u201335 (2014)","journal-title":"Reliab. Eng. Syst. Saf."},{"key":"16_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-3-642-38601-5_4","volume-title":"Reliable Software Technologies \u2013 Ada-Europe 2013","author":"C Brandon","year":"2013","unstructured":"Brandon, C., Chapin, P.: A SPARK\/Ada CubeSat control program. In: Keller, H.B., Pl\u00f6dereder, E., Dencker, P., Klenk, H. (eds.) Ada-Europe 2013. LNCS, vol. 7896, pp. 51\u201364. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-38601-5_4"},{"key":"16_CR15","unstructured":"California Polytechnic State University. CubeSat Design Specification Rev. 13 (2014). http:\/\/www.cubesat.org\/s\/cds_rev13_final2.pdf"},{"key":"16_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/978-3-642-01648-6_2","volume-title":"Models in Software Engineering","author":"MY Chkouri","year":"2009","unstructured":"Chkouri, M.Y., Robert, A., Bozga, M., Sifakis, J.: Translating AADL into BIP - application to the verification of real-time systems. In: Chaudron, M.R.V. (ed.) MODELS 2008. LNCS, vol. 5421, pp. 5\u201319. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-01648-6_2"},{"key":"16_CR17","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Dorigatti, M., Tonetta, S.: OCRA: a tool for checking the refinement of temporal contracts. In: ASE 2013, pp. 702\u2013705, November 2013","DOI":"10.1109\/ASE.2013.6693137"},{"key":"16_CR18","doi-asserted-by":"crossref","unstructured":"Dathathri, S., et al.: Interfacing TuLiP with the JPL statechart autocoder: initial progress toward synthesis of flight software from formal specifications. In: IEEE AeroSpace (2016)","DOI":"10.1109\/AERO.2016.7500557"},{"key":"16_CR19","volume-title":"Design Patterns: Elements of Reusable Object-Oriented Software","author":"E Gamma","year":"1994","unstructured":"Gamma, E., et al.: Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley Professional, Boston (1994)"},{"key":"16_CR20","unstructured":"Jung, A., Panunzio, M., Terraillon, J.-L.: On-board software reference architecture. Technical report TEC-SWE\/09-289\/AJ, SAVOIR Advisory Group (2010)"},{"key":"16_CR21","doi-asserted-by":"crossref","unstructured":"Kim, J.-S., Garlan, D.: Analyzing architectural styles with Alloy. In: ROSATEA 2006, pp. 70\u201380. ACM (2006)","DOI":"10.1145\/1147249.1147259"},{"key":"16_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/978-3-319-28934-2_14","volume-title":"Formal Aspects of Component Software","author":"A Mavridou","year":"2016","unstructured":"Mavridou, A., Baranov, E., Bliudze, S., Sifakis, J.: Configuration logics: modelling architecture styles. In: Braga, C., \u00d6lveczky, P.C. (eds.) FACS 2015. LNCS, vol. 9539, pp. 256\u2013274. Springer, Cham (2016). doi: 10.1007\/978-3-319-28934-2_14"},{"key":"16_CR23","unstructured":"Mavridou, A., et al.: Architecture-based Design: A Satellite On-Board Software Case Study. Technical report 221156, EPFL, September 2016. https:\/\/infoscience.epfl.ch\/record\/221156"},{"key":"16_CR24","doi-asserted-by":"crossref","unstructured":"Mavridou, A., et al.: Architecture diagrams: a graphical language for architecture style specification. In: 9th ICE, EPTCS, vol. 223, pp. 83\u201397 (2016)","DOI":"10.4204\/EPTCS.223.6"},{"issue":"1","key":"16_CR25","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1109\/32.825767","volume":"26","author":"N Medvidovic","year":"2000","unstructured":"Medvidovic, N., Taylor, R.N.: A classification and comparison framework for software architecture description languages. IEEE Trans. Softw. Eng. 26(1), 70\u201393 (2000)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"16_CR26","doi-asserted-by":"crossref","unstructured":"Mitchell, C., et al.: Development of a modular command and data handling architecture for the KySat-2 CubeSat. In: 2014 IEEE Aerospace Conference, pp. 1\u201311. IEEE, March 2014","DOI":"10.1109\/AERO.2014.6836355"},{"key":"16_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1007\/978-3-319-15317-9_18","volume-title":"Formal Aspects of Component Software","author":"M Noureddine","year":"2015","unstructured":"Noureddine, M., Jaber, M., Bliudze, S., Zaraket, F.A.: Reduction and abstraction techniques for BIP. In: Lanese, I., Madelaine, E. (eds.) FACS 2014. LNCS, vol. 8997, pp. 288\u2013305. Springer, Cham (2015). doi: 10.1007\/978-3-319-15317-9_18"},{"key":"16_CR28","doi-asserted-by":"crossref","unstructured":"Ozkaya, M., Kloukinas, C.: Are we there yet? analyzing architecture description languages for formal analysis, usability, and realizability. In: SEAA 2013, pp. 177\u2013184. IEEE (2013)","DOI":"10.1109\/SEAA.2013.34"},{"key":"16_CR29","unstructured":"Pagnamenta, M.: Rigorous software design for nano and micro satellites using BIP framework. Master\u2019s thesis, EPFL (2014). https:\/\/infoscience.epfl.ch\/record\/218902"},{"key":"16_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1007\/978-3-642-25264-8_4","volume-title":"SDL 2011: Integrating System and Software Modeling","author":"M Perrotin","year":"2011","unstructured":"Perrotin, M., Conquet, E., Delange, J., Schiele, A., Tsiodras, T.: TASTE: a real-time software engineering tool-chain overview, status, and future. In: Ober, I., Ober, I. (eds.) SDL 2011. LNCS, vol. 7083, pp. 26\u201337. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-25264-8_4"},{"key":"16_CR31","unstructured":"Rossi, S., et al.: CubETH magnetotorquers: design and tests for a CubeSat mission. In: Advances in the Astronautical Sciences, vol. 153, pp. 1513\u20131530 (2015)"},{"key":"16_CR32","unstructured":"Sifakis, J.: Rigorous system design. Found. $${\\rm Trends}^{\\textregistered }$$ Electron. Des. Autom. 6(4), 293\u2013362 (2012)"},{"key":"16_CR33","doi-asserted-by":"crossref","unstructured":"Spangelo, S.C., et al.: Model based systems engineering (MBSE) applied to Radio Aurora Explorer (RAX) CubeSat mission operational scenarios. In: 2013 IEEE Aerospace Conference, pp. 1\u201318. IEEE, March 2013","DOI":"10.1109\/AERO.2013.6496894"},{"key":"16_CR34","unstructured":"SysML. http:\/\/www.sysml.org"},{"key":"16_CR35","doi-asserted-by":"crossref","unstructured":"Woods, E., Hilliard, R.: Architecture description languages in practice session report. In: WICSA 2005, pp. 243\u2013246. IEEE Computer Society (2005)","DOI":"10.1109\/WICSA.2005.15"}],"container-title":["Lecture Notes in Computer Science","Formal Aspects of Component Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-57666-4_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,20]],"date-time":"2019-09-20T20:09:22Z","timestamp":1569010162000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-57666-4_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319576657","9783319576664"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-57666-4_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}