Formal verification of distributed controllers using Time-Stamped Event Count Automata

We study distributed controllers where sensor, controller, and actuator tasks are mapped onto different processors or Electronic Control Units (ECUs) in a distributed automotive architecture, communicating via a shared bus. Controllers in such setups are designed with a sampling period equal to the worst-case sensor-to-actuator message delay. However, this assumption of all messages having to meet their deadlines is too pessimistic. The inherent robustness of most controllers allows some of the messages to miss their deadlines, while still meeting specified control performance constraints. Given a controller, in this paper we first quantify the frequency of its acceptable deadline misses and represent this as a Linear Temporal Logic (LTL) formula. Further, we model the distributed architecture as a network of Time-Stamped Event Count Automata (TS-ECAs). Such a network of TS-ECAs is then model-checked to verify whether it satisfies the LTL formula. The verification ensures that the controller may be mapped onto the architecture and the control performance constraints will be satisfied. We have implemented this methodology in Symbolic Analysis Laboratory (SAL), which is a well-known framework combining different tools for system verification. Our implementation and case studies using standard controller design shows the applicability of our proposed controller/architecture co-verification. It represents a significant improvement in current design flows where, although controller models are formally verified, their implementation on a distributed architecture is done in an ad hoc fashion with extensive testing and integration effort.