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

Matthias Kauer, Sebastian Steinhorst, Dip Goswami, Reinhard Schneider, Martin Lukasiewycz, Samarjit Chakraborty

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

8 Citations (Scopus)

Abstract

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.
Original languageEnglish
Title of host publication2013 18th Asia and South Pacific Design Automation Conference (ASP-DAC)
Place of PublicationPiscataway
PublisherInstitute of Electrical and Electronics Engineers
Pages411-416
Number of pages6
ISBN (Electronic)978-1-4673-3030-5
ISBN (Print)978-1-4673-3029-9
DOIs
Publication statusPublished - 2013
Externally publishedYes
Event18th Asia and South Pacific Design Automation Conference, - Yokohama, Japan
Duration: 22 Jan 201325 Jan 2013

Conference

Conference18th Asia and South Pacific Design Automation Conference,
Abbreviated titleASP-DAC 2013
CountryJapan
CityYokohama
Period22/01/1325/01/13

Fingerprint Dive into the research topics of 'Formal verification of distributed controllers using Time-Stamped Event Count Automata'. Together they form a unique fingerprint.

  • Cite this

    Kauer, M., Steinhorst, S., Goswami, D., Schneider, R., Lukasiewycz, M., & Chakraborty, S. (2013). Formal verification of distributed controllers using Time-Stamped Event Count Automata. In 2013 18th Asia and South Pacific Design Automation Conference (ASP-DAC) (pp. 411-416). Piscataway: Institute of Electrical and Electronics Engineers. https://doi.org/10.1109/ASPDAC.2013.6509631