Static and Dynamic Verification of Space Systems Using Asynchronous Observer Agents
Formal verification of distributed systems is essential, especially in mission-critical systems that cannot be restarted. Such are space systems in which satellites read sensor values and autonomously make actuator decisions based on them, and ground services only set general patterns of behavior. T...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
MDPI AG
2021-07-01
|
| Series: | Sensors |
| Subjects: | |
| Online Access: | https://www.mdpi.com/1424-8220/21/13/4541 |
| _version_ | 1797527871425609728 |
|---|---|
| author | Wiktor B. Daszczuk |
| author_facet | Wiktor B. Daszczuk |
| author_sort | Wiktor B. Daszczuk |
| collection | DOAJ |
| description | Formal verification of distributed systems is essential, especially in mission-critical systems that cannot be restarted. Such are space systems in which satellites read sensor values and autonomously make actuator decisions based on them, and ground services only set general patterns of behavior. The verification formalism should correspond to the essential characteristics of a distributed system, such as node autonomy and asynchrony of actions and communication, as in our Integrated Model of Distributed Systems (IMDS). It is also crucial that the formalism allows for finding partial deadlocks and checking partial termination, where only a subset of the system nodes is involved while the rest can perform their own tasks at the same time. This article presents the idea of using monitoring agents—observers prepared in the IMDS formalism. Observers check the state of individual system components by polling, allowing verification without knowing the global state of the system. Such an agent is an ideal prototype of a runtime observer that checks if the actual operation of the system corresponds to a design that has previously been proven correct. |
| first_indexed | 2024-03-10T09:49:58Z |
| format | Article |
| id | doaj.art-8d899d597e1e4ae3a7b92347d69be72e |
| institution | Directory Open Access Journal |
| issn | 1424-8220 |
| language | English |
| last_indexed | 2024-03-10T09:49:58Z |
| publishDate | 2021-07-01 |
| publisher | MDPI AG |
| record_format | Article |
| series | Sensors |
| spelling | doaj.art-8d899d597e1e4ae3a7b92347d69be72e2023-11-22T02:50:53ZengMDPI AGSensors1424-82202021-07-012113454110.3390/s21134541Static and Dynamic Verification of Space Systems Using Asynchronous Observer AgentsWiktor B. Daszczuk0Institute of Computer Science, Warsaw University of Technology, Nowowiejska Str. 15/19, 00-665 Warsaw, PolandFormal verification of distributed systems is essential, especially in mission-critical systems that cannot be restarted. Such are space systems in which satellites read sensor values and autonomously make actuator decisions based on them, and ground services only set general patterns of behavior. The verification formalism should correspond to the essential characteristics of a distributed system, such as node autonomy and asynchrony of actions and communication, as in our Integrated Model of Distributed Systems (IMDS). It is also crucial that the formalism allows for finding partial deadlocks and checking partial termination, where only a subset of the system nodes is involved while the rest can perform their own tasks at the same time. This article presents the idea of using monitoring agents—observers prepared in the IMDS formalism. Observers check the state of individual system components by polling, allowing verification without knowing the global state of the system. Such an agent is an ideal prototype of a runtime observer that checks if the actual operation of the system corresponds to a design that has previously been proven correct.https://www.mdpi.com/1424-8220/21/13/4541modeling of space systemsverification of space systemsmonitoring agentsobserver agentsautomated test generation |
| spellingShingle | Wiktor B. Daszczuk Static and Dynamic Verification of Space Systems Using Asynchronous Observer Agents Sensors modeling of space systems verification of space systems monitoring agents observer agents automated test generation |
| title | Static and Dynamic Verification of Space Systems Using Asynchronous Observer Agents |
| title_full | Static and Dynamic Verification of Space Systems Using Asynchronous Observer Agents |
| title_fullStr | Static and Dynamic Verification of Space Systems Using Asynchronous Observer Agents |
| title_full_unstemmed | Static and Dynamic Verification of Space Systems Using Asynchronous Observer Agents |
| title_short | Static and Dynamic Verification of Space Systems Using Asynchronous Observer Agents |
| title_sort | static and dynamic verification of space systems using asynchronous observer agents |
| topic | modeling of space systems verification of space systems monitoring agents observer agents automated test generation |
| url | https://www.mdpi.com/1424-8220/21/13/4541 |
| work_keys_str_mv | AT wiktorbdaszczuk staticanddynamicverificationofspacesystemsusingasynchronousobserveragents |