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 generic and arise in domains such as automotive and industrial automation; they are multiple processors or electronic control units (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 tigher control performance properties compared to what would be possible with only worst-case delay bounds.
Original language | English |
---|---|
Title of host publication | DAC Design Automation Conference 2012 |
Place of Publication | Piscataway |
Publisher | Institute of Electrical and Electronics Engineers |
Pages | 688-696 |
Number of pages | 9 |
ISBN (Electronic) | 978-1-4503-1199-1 |
ISBN (Print) | 978-1-4503-1199-1 |
DOIs | |
Publication status | Published - 2012 |
Externally published | Yes |
Event | DAC Design Automation Conference 2012 - San Francisco, United States Duration: 3 Jun 2012 → 7 Jun 2012 |
Conference
Conference | DAC Design Automation Conference 2012 |
---|---|
Country/Territory | United States |
City | San Francisco |
Period | 3/06/12 → 7/06/12 |
Other | DAC 2012 |