A Hybrid Approach to Cyber-Physical Systems Veri cation
Pratyush Kumar, Dip oswami, Dipanjan Chakraborty, Kai Lampka, Anuradha Annaswamy, and Lothar Thiele.
In In Proceedings of the 49th Design Automation Conference, DAC 2012, San Fransisco, USA, June 2012. ACM
We propose a performance veri cation technique for cyber-physical systems that consist of multiple control loops implemented on a distributed architecture. The architectures we consider are fairly generic and arise in domains such as automotive and industrial automation; there are multiple processor or electronic control unites (ECUs) communicating over buses like FlexRay and CAN. Current practice involves analyzing the architecture to estimate worst-case end-to-end message delays and using these delays to design the control applications. This involves a significant amount of pessimism since the worst-case delays often occur very rarely. We show how to combine functional analysis techniques with model checking in order to derive a delay-frequency interface that quantifies the interleavings between messages with worst-case delays and those with smaller delays. In other words, we bound the frequency with which control messages might su er the worst-case delay. We show that such a delay-frequency interface enables us to verify much tighter control performance properties compares to the what would be possibly only with worst-case bounds.
