Model-Based Reliability, Availability, and Maintainability Analysis for Satellite Systems with Collaborative Maneuvers via Stochastic Games

被引：0

作者：

Baouya, Abdelhakim ^{[1
]}

Hamid, Brahim ^{[1
]}

Mohamed, Otmane Ait ^{[2
]}

Bensalem, Saddek ^{[3
]}

机构：

[1] Univ Toulouse, IRIT, CNRS, UT2, 118 Route Narbonne, F-31062 Toulouse 9, France

[2] Concordia Univ, Dept Elect & Comp Engn ECE, Montreal, PQ, Canada

[3] Univ Grenoble Alpes, VERIMAG, Grenoble, France

来源：

2024 50TH EUROMICRO CONFERENCE ON SOFTWARE ENGINEERING AND ADVANCED APPLICATIONS, SEAA 2024 | 2024年

关键词：

Navigation Satellite Systems; Reliability; Availability; Maintainability; Concurrent Stochastic Games;

D O I：

10.1109/SEAA64295.2024.00014

中图分类号：

TP39 [计算机的应用];

学科分类号：

081203 ; 0835 ;

摘要：

Space-based navigation systems rely on satellites to operate in orbit and have lifetimes of 10 years or more. Engineers employ Reliability, Availability, and Maintainability (RAM) analysis during the design phase to maximize a satellite's mean time between failures (MTBF). These design parameters help to optimize maintenance plans, enhance overall reliability, and extend the satellite's lifespan. The paper presents a novel approach using concurrent stochastic games (CSG) to model a single satellite with logical and formal specifications of RAM properties in rPATL. We leverage the PRISM-games model checker for quantitative analysis while considering collaborative behaviors between involved players in orbit and on the ground. This CSG-based approach offers a rich design space where actors considered as players involved in satellite maintenance can collaborate and learn optimal strategies.

引用

页码：27 / 34

页数：8

共 17 条

[1] Alternating-time temporal logic
Alur, R
Henzinger, TA
Kupferman, O
[J]. JOURNAL OF THE ACM, 2002, 49 (05) : 672 - 713
[2] Baier C., Principles of Model Checking
[3] Rigorous Security Analysis of RabbitMQ Broker with Concurrent Stochastic Games
Baouya, Abdelhakim
Hamid, Brahim
Guergen, Levent
Bensalem, Saddek
[J]. INTERNET OF THINGS, 2024, 26
[4] Reasoning about Human Participation in Self-Adaptive Systems
Camara, Javier
Moreno, Gabriel A.
Garlan, David
[J]. 2015 IEEE/ACM 10TH INTERNATIONAL SYMPOSIUM ON SOFTWARE ENGINEERING FOR ADAPTIVE AND SELF-MANAGING SYSTEMS, 2015, : 145 - 155
[5] Optimal Planning for Architecture-Based Self-Adaptation Via Model Checking of Stochastic Games
Camara, Javier
Garlan, David
Schmerl, Bradley
Pandey, Ashutosh
[J]. 30TH ANNUAL ACM SYMPOSIUM ON APPLIED COMPUTING, VOLS I AND II, 2015, : 428 - 435
[6] Chen T, 2012, LECT NOTES COMPUT SC, V7214, P315, DOI 10.1007/978-3-642-28756-5_22
[7] Hansson H., 1994, Formal Aspects of Computing, V6, P512, DOI 10.1007/BF01211866
[8] Hoque KA, 2015, DES AUT TEST EUROPE, P1635
[9] Kwiatkowska Marta, 2011, Computer Aided Verification. Proceedings 23rd International Conference, CAV 2011, P585, DOI 10.1007/978-3-642-22110-1_47
[10] Correlated Equilibria and Fairness in Concurrent Stochastic Games
Kwiatkowska, Marta
Norman, Gethin
Parker, David
Santos, Gabriel
[J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2022, PT II, 2022, 13244 : 60 - 78

← 1 2 →