{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,18]],"date-time":"2026-06-18T21:51:41Z","timestamp":1781819501995,"version":"3.54.5"},"reference-count":39,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T00:00:00Z","timestamp":1782864000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T00:00:00Z","timestamp":1782864000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2026,5,29]],"date-time":"2026-05-29T00:00:00Z","timestamp":1780012800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Array"],"published-print":{"date-parts":[[2026,7]]},"DOI":"10.1016\/j.array.2026.100966","type":"journal-article","created":{"date-parts":[[2026,5,29]],"date-time":"2026-05-29T16:04:18Z","timestamp":1780070658000},"page":"100966","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":0,"special_numbering":"C","title":["A generic algorithm for universal TDM communication over inter-satellite links: Foundations, verification, and practice"],"prefix":"10.1016","volume":"30","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8385-149X","authenticated-orcid":false,"given":"Miroslav","family":"Popovic","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-6346-0338","authenticated-orcid":false,"given":"Pavle","family":"Vasiljevic","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1957-0092","authenticated-orcid":false,"given":"Marko","family":"Popovic","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7563-3820","authenticated-orcid":false,"given":"Miodrag","family":"Djukic","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-5037-1055","authenticated-orcid":false,"given":"David","family":"V\u00e1zquez Enr\u00edquez","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-8345-3044","authenticated-orcid":false,"given":"Giovanni","family":"Granato","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-8467-5872","authenticated-orcid":false,"given":"Borja","family":"Lecue Cires","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"78","reference":[{"key":"10.1016\/j.array.2026.100966_bib1","series-title":"Proceedings of the 2023 Zooming Innovation in Consumer Technologies Conference, 2023","first-page":"148","article-title":"A simple python testbed for federated learning algorithms","author":"Popovic","year":"2023"},{"key":"10.1016\/j.array.2026.100966_bib4","series-title":"2024 32nd telecommunications forum (TELFOR), Belgrade, Serbia","first-page":"1","article-title":"MicroPython testbed for federated learning algorithms","author":"Popovic","year":"2024"},{"key":"10.1016\/j.array.2026.100966_bib5","first-page":"26","article-title":"A federated learning algorithms Development paradigm","volume":"vol. 14390","author":"Popovic","year":"2024"},{"key":"10.1016\/j.array.2026.100966_bib6","series-title":"2023 31st telecommunications forum (TELFOR)","first-page":"1","article-title":"Developing elementary federated learning algorithms leveraging the ChatGPT","author":"Popovic","year":"2023"},{"key":"10.1016\/j.array.2026.100966_bib7","first-page":"274","article-title":"Correct orchestration of federated learning generic algorithms: formalisation and verification in CSP","author":"Proki\u0107","year":"2023","journal-title":"Lect Notes Comput Sci"},{"key":"10.1016\/j.array.2026.100966_bib8","series-title":"Upper saddle River, NJ, USA","article-title":"Communicating sequential processes","author":"Hoare","year":"2004"},{"key":"10.1016\/j.array.2026.100966_bib9","series-title":"Computer Aided Verification (CAV 2009)","first-page":"709","article-title":"PAT: towards flexible verification under fairness","volume":"vol. 5643","author":"Liu","year":"2009"},{"issue":"6","key":"10.1016\/j.array.2026.100966_bib10","first-page":"929","article-title":"PAT: towards flexible verification of concurrent and real-time systems","volume":"36","author":"Sun","year":"2010","journal-title":"IEEE Trans Software Eng"},{"key":"10.1016\/j.array.2026.100966_bib11","series-title":"2025 33rd telecommunications forum (TELFOR), belgrade, Serbia","first-page":"1","article-title":"A generic algorithm for universal TDM communication over inter satellite links","author":"Popovic","year":"2025"},{"key":"10.1016\/j.array.2026.100966_bib12","series-title":"2025 33rd telecommunications forum (TELFOR), Belgrade, Serbia","first-page":"1","article-title":"Formal verification of a generic Algorithm for TDM communication over inter satellite links","author":"Popovic","year":"2025"},{"key":"10.1016\/j.array.2026.100966_bib13","series-title":"Proc. 32nd IEEE telecommunications forum","first-page":"1","article-title":"Towards formal verification of federated learning orchestration protocols on satellites","author":"Popovic","year":"2024"},{"key":"10.1016\/j.array.2026.100966_bib14","series-title":"Celestial Mechanics (textbook in Serbian)","author":"Milankovic","year":"1935"},{"key":"10.1016\/j.array.2026.100966_bib15","series-title":"Proc. of the 2016","first-page":"1","article-title":"Using timed automata to check space mission feasibility in the early design phases","author":"Akhundov","year":"2016"},{"key":"10.1016\/j.array.2026.100966_bib16","series-title":"Proc. of the 2023 ACM\/IEEE 26th International Conference on Model Driven Engineering Languages and Systems (MODELS)","article-title":"Applicability of model checking for verifying spacecraft operational designs","author":"Chrszon","year":"2023"},{"key":"10.1016\/j.array.2026.100966_bib17","first-page":"1","article-title":"Formalizing inter-satellite communication specification in small satellite System","volume":"20","author":"Gebreyohannes","year":"2016","journal-title":"the Proc of the Small Satellites, System & Services Symposium (4S)"},{"key":"10.1016\/j.array.2026.100966_bib18","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"26","DOI":"10.1007\/978-3-642-25264-8_4","article-title":"TASTE: a real-time software engineering tool-chain overview, status, and future","author":"Perrotin","year":"2011"},{"key":"10.1016\/j.array.2026.100966_bib19","series-title":"Proc. 2nd workshop on model-based space systems and software engineering (MBSE 2021)","article-title":"Specification and model-checking of space systems with TASTE","author":"Dragomir","year":"2021"},{"issue":"3","key":"10.1016\/j.array.2026.100966_bib20","doi-asserted-by":"crossref","first-page":"961","DOI":"10.1007\/s11334-025-00607-3","article-title":"Specification and model-checking of space systems in the TASTE toolset","volume":"21","author":"Dragomir","year":"2025","journal-title":"Innovat Syst Software Eng"},{"key":"10.1016\/j.array.2026.100966_bib21","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1007\/978-3-540-30080-9_8","article-title":"The IF toolset","author":"Bozga","year":"2004"},{"key":"10.1016\/j.array.2026.100966_bib22","series-title":"A formal approach to specifying and verifying spacecraft behavior","author":"McInnes","year":"2007"},{"key":"10.1016\/j.array.2026.100966_bib23","series-title":"Tools and algorithms for the construction and analysis of systems (TACAS 2014)","first-page":"187","article-title":"FDR3 \u2014 a modern refinement checker for CSP","volume":"vol.8413","author":"Gibson-Robinson","year":"2014"},{"issue":"4","key":"10.1016\/j.array.2026.100966_bib24","doi-asserted-by":"crossref","first-page":"626","DOI":"10.1145\/242223.242257","article-title":"Formal methods","volume":"28","author":"Clarke","year":"1996","journal-title":"ACM Comput Surv"},{"issue":"4","key":"10.1016\/j.array.2026.100966_bib25","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1592434.1592436","article-title":"\u201cFormal methods,\u201d ACM computing","volume":"41","author":"Woodcock","year":"2009","journal-title":"Surveys"},{"key":"10.1016\/j.array.2026.100966_bib26","doi-asserted-by":"crossref","first-page":"1551","DOI":"10.1016\/j.procs.2018.08.128","article-title":"Formal verification approaches for distributed algorithms: a systematic literature review","volume":"126","author":"Fakhfakh","year":"2018","journal-title":"Procedia Comput Sci"},{"issue":"1","key":"10.1016\/j.array.2026.100966_bib27","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1007\/BF00121261","article-title":"Automatic verification of distributed systems: the process algebra approach","volume":"8","author":"Inverardi","year":"1996","journal-title":"Formal Methods Syst Des"},{"key":"10.1016\/j.array.2026.100966_bib28","series-title":"2009 third IEEE international symposium on theoretical aspects of software engineering. IEEE","first-page":"81","article-title":"Verification of population ring protocols in PAT","author":"Liu","year":"2009"},{"key":"10.1016\/j.array.2026.100966_bib29","doi-asserted-by":"crossref","first-page":"342","DOI":"10.18293\/SEKE2018-067","article-title":"Modeling and verifying leader election algorithm in CSP (S)","volume":"2018","author":"Fang","year":"2018","journal-title":"International Conferences on Software Engineering and Knowledge Engineering"},{"key":"10.1016\/j.array.2026.100966_bib30","doi-asserted-by":"crossref","first-page":"158","DOI":"10.1007\/978-3-031-29927-8_13","article-title":"Formalization and verification of SIP using CSP","author":"Hou","year":"2023","journal-title":"Lect Notes Comput Sci"},{"key":"10.1016\/j.array.2026.100966_bib31","series-title":"Proceedings of the 6th international symposium on software engineering for adaptive and self-managing systems","first-page":"158","article-title":"A CSP-based framework for the specification, verification, and implementation of adaptive systems","author":"Bartels","year":"2011"},{"key":"10.1016\/j.array.2026.100966_bib32","series-title":"Formal Methods Europe (FME 2003), vol. 2805, ser. Lecture Notes in Computer Science","first-page":"855","article-title":"ProB: a model checker for B","author":"Leuschel","year":"2003"},{"key":"10.1016\/j.array.2026.100966_bib33","doi-asserted-by":"crossref","DOI":"10.1016\/j.jss.2020.110559","article-title":"Formal analysis and verification of the PSTM architecture using CSP","volume":"165","author":"Liu","year":"2020","journal-title":"J Syst Software"},{"key":"10.1016\/j.array.2026.100966_bib34","doi-asserted-by":"crossref","DOI":"10.1016\/j.jss.2025.112655","article-title":"Experimenting architectural patterns in federated learning systems","volume":"232","author":"Compagnucci","year":"2026","journal-title":"J Syst Software"},{"key":"10.1016\/j.array.2026.100966_bib35","series-title":"Discrete mathematics with combinatorics","isbn-type":"print","author":"Anderson","year":"2004","ISBN":"https:\/\/id.crossref.org\/isbn\/0130457914"},{"issue":"2","key":"10.1016\/j.array.2026.100966_bib36","doi-asserted-by":"crossref","first-page":"4961","DOI":"10.1109\/TAES.2024.3512535","article-title":"3 ISL topology: Routing Properties and Performance in LEO Megaconstellation Networks","volume":"61","author":"Chen","year":"2025","journal-title":"IEEE Trans Aero Electron Syst"},{"issue":"21","key":"10.1016\/j.array.2026.100966_bib37","doi-asserted-by":"crossref","first-page":"34554","DOI":"10.1109\/JIOT.2024.3452787","article-title":"Analysis of laser intersatellite links and topology design for mega-constellation networks","volume":"11","author":"Yang","year":"2024","journal-title":"IEEE Internet Things J"},{"key":"10.1016\/j.array.2026.100966_bib38","series-title":"Proceedings of the 2nd international workshop on LEO networking and communication","first-page":"1","article-title":"An In-Depth investigation of LEO satellite topology design parameters","author":"Zhang","year":"2024"},{"key":"10.1016\/j.array.2026.100966_bib39","series-title":"Ieee INFOCOM 2023 - IEEE Conference on Computer Communications","first-page":"1","article-title":"Network characteristics of LEO satellite constellations: a starlink-based measurement from end users","author":"Ma","year":"2023"},{"key":"10.1016\/j.array.2026.100966_bib40","series-title":"Ieee INFOCOM 2025 - IEEE Conference on Computer Communications","first-page":"1","article-title":"BAROC: concealing packet losses in LSNs with bimodal behavior awareness for livecast ingestion","author":"Zhao","year":"2025"},{"key":"10.1016\/j.array.2026.100966_bib41","unstructured":"\u201cSwarm Workshop,\u201d Swarm Workshop, Nov 27, 2025. https:\/\/swarmworkshop.eu (accessed November 28, 2025)."}],"container-title":["Array"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S2590005626002894?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S2590005626002894?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2026,6,18]],"date-time":"2026-06-18T20:56:04Z","timestamp":1781816164000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S2590005626002894"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,7]]},"references-count":39,"alternative-id":["S2590005626002894"],"URL":"https:\/\/doi.org\/10.1016\/j.array.2026.100966","relation":{},"ISSN":["2590-0056"],"issn-type":[{"value":"2590-0056","type":"print"}],"subject":[],"published":{"date-parts":[[2026,7]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"A generic algorithm for universal TDM communication over inter-satellite links: Foundations, verification, and practice","name":"articletitle","label":"Article Title"},{"value":"Array","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.array.2026.100966","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"\u00a9 2026 The Authors. Published by Elsevier Inc.","name":"copyright","label":"Copyright"}],"article-number":"100966"}}