@inproceedings{b4c5f294a8ba42e1a6d32d53bf6a351e,
title = "Soundness of the quasi-synchronous abstraction",
abstract = "Many critical real-time embedded systems are implemented as a set of processes that execute periodically with bounded jitter and communicate with bounded transmission delay. The quasi-synchronous abstraction was introduced by P. Caspi for model-checking the safety properties of applications running on such systems. The simplicity of the abstraction is appealing: The only events are process activations; logical steps account for transmission delays; and no process may be activated more than twice between two successive activations of any other. We formalize the relation between the real-time model and the quasi-synchronous abstraction by introducing the notion of a unitary discretization. Even though the abstraction has been applied several times in the literature, we show, surprisingly, that it is not sound for general systems of more than two processes. Our central result is to propose necessary and sufficient conditions on both communication topologies and timing parameters to recover soundness.",
author = "Guillaume Baudart and Timothy Bourke and Marc Pouzet",
note = "Publisher Copyright: {\textcopyright} 2016 FMCAD Inc.; 16th Conference on Formal Methods in Computer-Aided Design, FMCAD 2016 ; Conference date: 03-10-2016 Through 06-10-2016",
year = "2017",
month = mar,
day = "24",
doi = "10.1109/FMCAD.2016.7886655",
language = "English",
series = "Proceedings of the 16th Conference on Formal Methods in Computer-Aided Design, FMCAD 2016",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
pages = "9--16",
editor = "Ruzica Piskac and Muralidhar Talupur",
booktitle = "Proceedings of the 16th Conference on Formal Methods in Computer-Aided Design, FMCAD 2016",
}