{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,21]],"date-time":"2026-05-21T09:07:28Z","timestamp":1779354448993,"version":"3.51.4"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032267511","type":"print"},{"value":"9783032267528","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-26752-8_5","type":"book-chapter","created":{"date-parts":[[2026,5,21]],"date-time":"2026-05-21T08:11:36Z","timestamp":1779351096000},"page":"70-88","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Security-Minded Modelling and\u00a0Verification of\u00a0Autonomous Satellite Docking"],"prefix":"10.1007","author":[{"given":"Juel","family":"Hussain","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Louise A.","family":"Dennis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Clare","family":"Dixon","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marie","family":"Farrell","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2026,5,22]]},"reference":[{"key":"5_CR1","doi-asserted-by":"crossref","unstructured":"Aizatulin, M., Gordon, A.D., J\u00fcrjens, J.: Extracting and verifying cryptographic models from C protocol code by symbolic execution. In: Proceedings of the 18th ACM Conference on Computer and Communications Security (CCS), pp. 331\u2013340. ACM (2011)","DOI":"10.1145\/2046707.2046745"},{"key":"5_CR2","unstructured":"Akin, D.L., Scheeres, D.J., Whittaker, W.L.: Orbital express demonstration manipulator system (OEDMS): autonomous rendezvous and on-orbit servicing. In: Proceedings of the IEEE Aerospace Conference. IEEE (2008)"},{"key":"5_CR3","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"5_CR4","unstructured":"Basin, D., Dreier, J., Hirschi, L., Radomirovic, S., Sasse, R., Stettler, V.: Tamarin Prover Manual. ETH Zurich (2018)"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"B\u00f6rger, E.: The abstract state machines method for high-level system design and analysis. In: Formal Methods: State of the Art and New Directions, pp. 79\u2013116. Springer (2009)","DOI":"10.1007\/978-1-84882-736-3_3"},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"Braghin, C., Del Castillo, G., Riccobene, E., Valentini, S.: Using symbolic model execution to detect vulnerabilities of smart contracts. In: Leuschel, M., Ishikawa, F. (eds.) Rigorous State-Based Methods, pp. 31\u201351. Springer, Cham (2026)","DOI":"10.1007\/978-3-031-94533-5_3"},{"key":"5_CR7","unstructured":"Cardoso, R., et al.: Verification for Space Robotics. IET Cyber-Physical Systems: Theory & Applications (2024)"},{"key":"5_CR8","doi-asserted-by":"crossref","unstructured":"Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N., S\u00e1nchez, C.: Temporal logics for hyperproperties. In: Principles of Security and Trust, pp. 265\u2013284. Springer, Heidelberg (2014)","DOI":"10.1007\/978-3-642-54792-8_15"},{"issue":"6","key":"5_CR9","doi-asserted-by":"publisher","first-page":"1157","DOI":"10.3233\/JCS-2009-0393","volume":"18","author":"MR Clarkson","year":"2010","unstructured":"Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur. 18(6), 1157\u20131210 (2010)","journal-title":"J. Comput. Secur."},{"issue":"4","key":"5_CR10","doi-asserted-by":"publisher","first-page":"4048","DOI":"10.1109\/TDSC.2023.3345543","volume":"21","author":"M Farrell","year":"2024","unstructured":"Farrell, M., et al.: Security-minded verification of cooperative awareness messages. IEEE Trans. Dependable Secure Comput. 21(4), 4048\u20134065 (2024). https:\/\/doi.org\/10.1109\/TDSC.2023.3345543","journal-title":"IEEE Trans. Dependable Secure Comput."},{"key":"5_CR11","unstructured":"Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, Boston (2003)"},{"key":"5_CR12","unstructured":"Hussain, J.: Autonomous Satellite Docking - Security Verification Promela Code (2025). https:\/\/github.com\/juelhussain\/autosecver-docking. Accessed 2026"},{"key":"5_CR13","unstructured":"Khurshid, A., Zou, X., Zhou, W., Caesar, M., Godfrey, P.B.: VeriFlow: verifying network-wide invariants in real time. In: Proceedings of the 10th USENIX Symposium on Networked Systems Design and Implementation (NSDI), pp. 15\u201327. USENIX (2013)"},{"issue":"5","key":"5_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3342355","volume":"52","author":"M Luckcuck","year":"2019","unstructured":"Luckcuck, M., Farrell, M., Dennis, L., Dixon, C., Fisher, M.: Formal specification and verification of autonomous robotic systems: a survey. ACM Comput. Surv. 52(5), 1\u201341 (2019). https:\/\/doi.org\/10.1145\/3342355","journal-title":"ACM Comput. Surv."},{"key":"5_CR15","doi-asserted-by":"publisher","unstructured":"Malik, R., Mohajerani, S., Fabian, M.: A survey on compositional algorithms for verification and synthesis in supervisory control. Discret. Event Dyn. Syst. 33(3), 279\u2013340 (2023). https:\/\/doi.org\/10.1007\/s10626-023-00378-8","DOI":"10.1007\/s10626-023-00378-8"},{"key":"5_CR16","doi-asserted-by":"publisher","unstructured":"Maple, C., et al.: Security-minded verification of space systems. In: Proceedings of the IEEE Aerospace Conference. IEEE (2020). https:\/\/doi.org\/10.1109\/AERO47225.2020.9172563","DOI":"10.1109\/AERO47225.2020.9172563"},{"key":"5_CR17","doi-asserted-by":"crossref","unstructured":"Merkow, M.S., Raghavan, L.: Secure and Resilient Software: Requirements, Test Cases, and Testing Methods. CRC Press (2012)","DOI":"10.1201\/b11317"},{"key":"5_CR18","unstructured":"MITRE Corporation: Common Attack Pattern Enumeration and Classification (CAPEC). https:\/\/capec.mitre.org. Accessed 2026"},{"key":"5_CR19","unstructured":"MITRE Corporation: MITRE ATT&CK Framework: Adversarial Tactics, Techniques, and Common Knowledge. https:\/\/attack.mitre.org. Accessed 2026"},{"key":"5_CR20","doi-asserted-by":"publisher","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science (SFCS 1977), pp. 46\u201357 (1977). https:\/\/doi.org\/10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"key":"5_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-031-33163-3_6","volume-title":"Rigorous State-Based Methods","author":"G Schellhorn","year":"2023","unstructured":"Schellhorn, G., Bodenm\u00fcller, S., Reif, W.: Thread-local, step-local proof obligations for\u00a0refinement of\u00a0state-based concurrent systems. In: Gl\u00e4sser, U., Creissac Campos, J., M\u00e9ry, D., Palanque, P. (eds.) ABZ 2023. LNCS, vol. 14010, pp. 70\u201387. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-33163-3_6"},{"key":"5_CR22","unstructured":"Schneier, B.: Attack Trees (1999). https:\/\/www.schneier.com\/academic\/archives\/1999\/12\/attack_trees.html. Accessed 2026"},{"key":"5_CR23","unstructured":"Shostack, A.: Threat Modeling: Designing for Security. Wiley (2014)"},{"key":"5_CR24","doi-asserted-by":"publisher","unstructured":"Taylor, R.G., Foster, M., North, S.: An automated framework for verifying or refuting trace properties of extended finite state machines. Int. J. Softw. Tools Technol. Transf. 24(6), 949\u2013972 (2022). https:\/\/doi.org\/10.1007\/s10009-022-00666-y","DOI":"10.1007\/s10009-022-00666-y"}],"container-title":["Lecture Notes in Computer Science","Rigorous State-Based Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-26752-8_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,21]],"date-time":"2026-05-21T08:11:44Z","timestamp":1779351104000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-26752-8_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032267511","9783032267528"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-26752-8_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"22 May 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ABZ","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Rigorous State-Based Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Tokyo","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 May 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 May 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"abz2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/abz-conf.org\/site\/2026\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}