{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,24]],"date-time":"2026-07-24T15:20:14Z","timestamp":1784906414439,"version":"3.55.0"},"reference-count":39,"publisher":"MDPI AG","issue":"13","license":[{"start":{"date-parts":[[2023,7,5]],"date-time":"2023-07-05T00:00:00Z","timestamp":1688515200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100012190","name":"Ministry of Science and Higher Education of the Russian Federation","doi-asserted-by":"publisher","award":["FSRF-2023-0003"],"award-info":[{"award-number":["FSRF-2023-0003"]}],"id":[{"id":"10.13039\/501100012190","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Sensors"],"abstract":"<jats:p>Various methods of spatial redundancy can be used in local networks based on the SpaceFibre standard for fault mitigation of network hardware and physical communication channels. Usually, a network developer chooses the method of spatial redundancy according to the number of failures that have to be mitigated, the time required for restoring the normal operation of the network, required overheads and hardware costs. The use of different spatial redundancy mechanisms can cause changes in the structure of the links between network nodes, in case of failure and subsequent mitigation. In turn, this may cause changes in the broadcast transmission paths and the temporal characteristics of their delivery from the source to the receivers. This article focuses on the change in the propagation time of broadcasts in SpaceFibre networks with spatial redundancy. Broadcast propagation rules significantly differ from data-packet propagation rules. Broadcast distribution time is very important for many applications, because broadcasts are generally used to send urgent messages, in particular for time synchronization. Various formal methods have been used to evaluate the propagation characteristics of the broadcast. A method for estimating broadcast propagation time along the shortest routes is proposed. In addition, we provide a formal method to estimate the number of failures, which occurred in the network during the broadcast propagation. This method is based on timed Petri nets; one of its features is the ability to calculate broadcast transmission delays. In addition, as an alternative solution, we propose a method for estimating delays based on time automata theory.<\/jats:p>","DOI":"10.3390\/s23136161","type":"journal-article","created":{"date-parts":[[2023,7,6]],"date-time":"2023-07-06T00:54:41Z","timestamp":1688604881000},"page":"6161","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Broadcast Propagation Time in SpaceFibre Networks with Various Types of Spatial Redundancy"],"prefix":"10.3390","volume":"23","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1817-2754","authenticated-orcid":false,"given":"Valentin","family":"Olenev","sequence":"first","affiliation":[{"name":"Aerospace R&D Centre, Saint-Petersburg State University of Aerospace Instrumentation (SUAI), 190000 Saint-Petersburg, Russia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Elena","family":"Suvorova","sequence":"additional","affiliation":[{"name":"Aerospace R&D Centre, Saint-Petersburg State University of Aerospace Instrumentation (SUAI), 190000 Saint-Petersburg, Russia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nadezhda","family":"Chumakova","sequence":"additional","affiliation":[{"name":"Aerospace R&D Centre, Saint-Petersburg State University of Aerospace Instrumentation (SUAI), 190000 Saint-Petersburg, Russia"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"1968","published-online":{"date-parts":[[2023,7,5]]},"reference":[{"key":"ref_1","unstructured":"(2019). SpaceFibre\u2014Very high-Speed Serial Link (Standard No. ECSS-E-ST-50-11C)."},{"key":"ref_2","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","article-title":"A theory of timed automata","volume":"126","author":"Alur","year":"1994","journal-title":"Theor. Comp. Sci."},{"key":"ref_3","unstructured":"Karpov, Y.G. (2010). Verification of Parallel and Distributed Software Systems, BHV."},{"key":"ref_4","first-page":"59","article-title":"Model Checking Reconfigurable Interacting Systems","volume":"Volume 13703","author":"Margaria","year":"2022","journal-title":"Leveraging Applications of Formal Methods, Verification and Validation. Adaptation and Learning"},{"key":"ref_5","unstructured":"Velder, S.E., Lukin, M.A., Shalyto, A.A., and Yaminov, B.R. (2011). Verification of Automata-Based Programs, Science."},{"key":"ref_6","unstructured":"Govind, R., Herbreteau, F., Srivathsan, B., and Walukiewicz, I. (August, January 31). Abstractions for the local-time semantics of timed automata: A foundation for partial-order methods. Proceedings of the 37th Annual ACM\/IEEE Symposium on Logic in Computer Science, Haifa, Israel."},{"key":"ref_7","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1016\/j.tcs.2003.10.038","article-title":"Optimal Paths in Weighted Timed Automata","volume":"318","author":"Alur","year":"2004","journal-title":"Theor. Comp. Sci."},{"key":"ref_8","first-page":"400","article-title":"Decision Problems for Parametric Timed Automata","volume":"Volume 10009","author":"Ogata","year":"2016","journal-title":"ICFEM: Formal Methods and Software Engineering. Lecture Notes in Computer Science"},{"key":"ref_9","first-page":"37","article-title":"TCTL model checking lower\/upper-bound parametric timed automata without invariants","volume":"Volume 11022","author":"Jansen","year":"2018","journal-title":"FORMATS: Formal Modeling and Analysis of Timed Systems. Lecture Notes in Computer Science"},{"key":"ref_10","first-page":"381","article-title":"Monte Carlo Tree Search for Priced Timed Automata","volume":"Volume 13479","author":"Paolieri","year":"2022","journal-title":"Quantitative Evaluation of Systems, Proceedings of the 19th International Conference (QEST 2022), Warsaw, Poland, 13\u201316 September 2022"},{"key":"ref_11","first-page":"69","article-title":"Language Emptiness of Continuous-Time Parametric Timed Automata","volume":"Volume 9135","author":"Larsen","year":"2015","journal-title":"Part II. Automata, Languages, and Programming, Lecture Notes in Computer Science, Proceedings of the 42nd International Colloquium, ICALP 2015, Kyoto, Japan, 6\u201310 July 2015"},{"key":"ref_12","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1007\/s10009-017-0467-0","article-title":"What\u2019s decidable about parametric timed automata?","volume":"21","year":"2019","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"ref_13","unstructured":"Chakraborty, S., Phan, L.T.H., and Thiagarajan, P.S. (2005, January 5\u20138). Event Count Automata: A State-based Model for Stream Processing Systems. Proceedings of the 26th IEEE International Real-Time Systems Symposium, Miami, FL, USA."},{"key":"ref_14","doi-asserted-by":"crossref","unstructured":"Boyer, M., and Roux, P. (2016, January 6\u20139). Embedding network calculus and event stream theory in a common model. Proceedings of the 21st International Conference on Emerging Technologies and Factory Automation (ETFA), Berlin, Germany.","DOI":"10.1109\/ETFA.2016.7733565"},{"key":"ref_15","first-page":"1","article-title":"Timed automata based modeling and verification of denial of service attacks in wireless sensor networks","volume":"12","author":"Hammal","year":"2014","journal-title":"Stud. Inform. Univ."},{"key":"ref_16","unstructured":"Anand, M., Dajani-Brown, S., Vestal, S., and Lee, I. (2006, January 24\u201326). Formal Modeling and Analysis of AFDX Frame Management Design. Proceedings of the 9th International Symposium on Object-Oriented Real-Time Distributed Computing, Gyeongju, Republic of Korea."},{"key":"ref_17","unstructured":"Govind, R., Herbreteau, F., Srivathsan, B., and Walukiewicz, I. (2019, January 27\u201330). Revisiting local time semantics for networks of timed automata. Proceedings of the 30th International Conference on Concurrency Theory, Amsterdam, The Netherlands."},{"key":"ref_18","first-page":"13:1","article-title":"Simulations for Event-Clock Automata","volume":"Volume 243","author":"Klin","year":"2022","journal-title":"Proceedings of the 33rd International Conference on Concurrency Theory"},{"key":"ref_19","first-page":"59","article-title":"Breaking Down High-Level Robot Path-Finding Abstractions in Natural Language Programming","volume":"Volume 12414","author":"Baldoni","year":"2021","journal-title":"Advances in Artificial Intelligence"},{"key":"ref_20","unstructured":"Sherwani, N. (1998). Algorithms for VLSI Physical Design Automation, Springer. [3rd ed.]."},{"key":"ref_21","doi-asserted-by":"crossref","first-page":"313","DOI":"10.1016\/j.actaastro.2020.06.041","article-title":"A representative SpaceFibre network evaluation: Features, performances and future trends","volume":"176","author":"Nannipieri","year":"2020","journal-title":"Acta Astronaut."},{"key":"ref_22","doi-asserted-by":"crossref","first-page":"9","DOI":"10.1109\/JPROC.2006.887290","article-title":"Control and Communication Challenges in Networked Real-Time Systems","volume":"95","author":"Baillieul","year":"2007","journal-title":"Proc. IEEE"},{"key":"ref_23","doi-asserted-by":"crossref","unstructured":"Shooman, M.L. (2002). Reliability of Computer Systems and Networks: Fault Tolerance, Analysis, and Design, John Wiley & Sons, Inc.","DOI":"10.1002\/047122460X"},{"key":"ref_24","doi-asserted-by":"crossref","unstructured":"Alena, R.L., Ossenfort, J.P., Laws, K.I., and Goforth, A. (2007, January 3\u201310). Communications for Integrated Modular Avionics. Proceedings of the IEEE Conference on Aerospace, Big Sky, MT, USA.","DOI":"10.1109\/AERO.2007.352639"},{"key":"ref_25","unstructured":"Butz, H. (2007). Aircraft Systems Technician, Aviation Supplies & Academics Inc."},{"key":"ref_26","unstructured":"Aeronautical Radio Inc. (2005). Aircraft Data Network Part 7: Avionics Full-Duplex Switched Ethernet (AFDX), Aeronautical Radio, Inc.. Network. ARINC Specification 664, Part 7."},{"key":"ref_27","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3570326","article-title":"Scheduling of Resource Allocation Systems with Timed Petri Nets: A Survey","volume":"55","author":"Huang","year":"2023","journal-title":"ACM Comp. Surv."},{"key":"ref_28","first-page":"212","article-title":"Modeling of safe timed Petri nets by two-level (max,+) automata","volume":"55","author":"Komenda","year":"2022","journal-title":"IFAC"},{"key":"ref_29","first-page":"37","article-title":"A methodology for formalized development of communication protocols based on Petri nets","volume":"4","author":"Olenev","year":"2022","journal-title":"Inf. Space"},{"key":"ref_30","first-page":"405","article-title":"KReach: A Tool for Reachability in Petri Nets","volume":"Volume 12078","author":"Biere","year":"2020","journal-title":"Tools and Algorithms for the Construction and Analysis of Systems, Proceedings of the 28th International Conference, Munich, Germany, 2\u20137 April 2022"},{"key":"ref_31","doi-asserted-by":"crossref","unstructured":"Liu, G. (2022). Petri Nets: Theoretical Models and Analysis Methods for Concurrent Systems, Springer.","DOI":"10.1007\/978-981-19-6309-4"},{"key":"ref_32","doi-asserted-by":"crossref","first-page":"174","DOI":"10.18255\/1818-1015-2018-2-174-192","article-title":"On the Correctness of Real-Time Modular Computer Systems Modeling with Stopwatch Automata Networks","volume":"25","author":"Glonina","year":"2018","journal-title":"Model. Anal. Inf. Syst."},{"key":"ref_33","unstructured":"Glonina, A.B. (2020). A Tool System for Schedulability Analysis of Modular Computer Systems Configurations, Lomonosov Moscow State Universisty."},{"key":"ref_34","first-page":"43","article-title":"General model of real-time modular computer systems operation for checking acceptability of such systems configurations","volume":"Volume 6","author":"Glonina","year":"2018","journal-title":"Bulletin of the South Ural State University, Series: Mathematical Modelling, Programming and Computer Software"},{"key":"ref_35","doi-asserted-by":"crossref","unstructured":"Tigane, S., Guerrouf, F., Hamani, N., Kahloul, L., Khalgui, M., and Ali, M.A. (2023). Dynamic Timed Automata for Reconfigurable System Modeling and Verification. Axioms, 12.","DOI":"10.3390\/axioms12030230"},{"key":"ref_36","doi-asserted-by":"crossref","unstructured":"Bettira, R., Kahloul, L., Khalgui, M., and Li, Z. (2019, January 6\u20139). Reconfigurable Hierarchical Timed Automata: Modeling and Stochastic Verification. Proceedings of the 2019 IEEE International Conference on Systems, Man, and Cybernetics, Bari, Italy.","DOI":"10.1109\/SMC.2019.8913890"},{"key":"ref_37","doi-asserted-by":"crossref","unstructured":"Bettira, R., Kahloul, L., and Khalgui, M. (2020, January 5\u20136). A Novel Approach for Repairing Reconfigurable Hierarchical Timed Automata. Proceedings of the 15th International Conference on Evaluation of Novel Approaches to Software Engineering, Prague, Czech Republic.","DOI":"10.5220\/0009408503980406"},{"key":"ref_38","doi-asserted-by":"crossref","unstructured":"Tahiri, I., Philippot, A., Carre-Menetrier, V., and Tajer, A. (2019, January 23). TimeBased Estimator for Control Reconfiguration of Discrete Event Systems (DES). Proceedings of the CoDIT 2019: International Conference on Control, Decision and Information Technologies, Paris, France.","DOI":"10.1109\/CoDIT.2019.8820585"},{"key":"ref_39","unstructured":"UPPAAL (2023, June 05). Online Documentation. Available online: https:\/\/uppaal.org\/documentation."}],"container-title":["Sensors"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/1424-8220\/23\/13\/6161\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T20:06:23Z","timestamp":1760126783000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/1424-8220\/23\/13\/6161"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,7,5]]},"references-count":39,"journal-issue":{"issue":"13","published-online":{"date-parts":[[2023,7]]}},"alternative-id":["s23136161"],"URL":"https:\/\/doi.org\/10.3390\/s23136161","relation":{},"ISSN":["1424-8220"],"issn-type":[{"value":"1424-8220","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,7,5]]}}}