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 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.