Verification of distributed systems through the analysis of communication data

Preliminary ideas

Abstract

This work presents preliminary ideas for the formal analysis of distributed systems, leveraging communication-derived observational data to verify system behavior. Our methodology synthesizes formal specification and runtime verification, with specifications expressed in a domain-specific language rooted in first-order logic and regular programs, akin to what is found in first-order dynamic logic. Building on this formalism, we designed and implemented a prototype tool that employs runtime verification to analyze data logged during the execution of the system, enabling both offline (post-mortem) analysis and run-time behavioral verification. To validate our approach, we conducted an initial experimental evaluation using telemetry data from a satellite CAN bus (developed by INVAP S.E.), a mission-critical aerospace system. Initial results demonstrate the framework’s capability to detect deviations from specified behavior.