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