Static and Dynamic Verification of Space Systems Using Asynchronous Observer Agents.

ABSTRACT: 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

SUBMITTER: Daszczuk WB 

PROVIDER: S-EPMC8271994 | biostudies-literature | 2021 Jul

REPOSITORIES: biostudies-literature