 |
|
|||
| Authors: | Pratyush Kumar, Dip Goswami, Samarjit Chakraborty, Anuradha Annaswamy, Kai Lampka, Lothar Thiele |
| Group: | Computer Engineering |
| Type: | Inproceedings |
| Title: | A Hybrid Approach to Cyber-Physical Systems Verification |
| Year: | 2012 |
| Month: | June |
| Pub-Key: | KGCLAT12 |
| Book Titel: | In Proceedings of the 49th Design Automation Conference, DAC 2012 |
| Pages: | 688-696 |
| Keywords: | CPS, Verification, RTC |
| Publisher: | ACM |
| Abstract: | We propose a performance verification technique for cyber-physical systems that consist of multiple control loops implemented on a distributed architecture. The architectures we consider are fairly genric 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 suffer 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 p0ossibly only with worst-case bounds. |
| Location: | San Fransisco, USA |
| Resources: | [BibTeX] [Paper as PDF] |
