@inproceedings{5dba8f14866a48c8bb393dfb3f3a7162,
title = "Effective System Level Liveness Verification",
abstract = "The language xMAS has been designed by Intel with the purpose of modelling and verification of hardware. Recently, the language was extended with finite state machines to make it more expressive [19]. Furthermore, it was shown how to prove liveness of such extended xMAS networks [19]. Unfortunately, we demonstrate that the proof technique is unsound. We provide an alternative approach which we have carefully proven to be correct. Moreover, we show that our approach scales very well, which makes it possible to prove liveness properties at the system level. In particular, we show that using our approach, it is possible to verify a power control architecture composed of 1299 state machines representing 50 power domains where each domain contains 5 master and 5 slave devices. Proving liveness of this system takes less than 10 minutes.",
keywords = "Formal verification, communication networks, finite state machines, liveness",
author = "Alexander Fedotov and Keiren, {Jeroen J.A.} and Julien Schmaltz",
year = "2020",
month = sep,
day = "21",
doi = "10.34727/2020/isbn.978-3-85448-042-6_7",
language = "English",
pages = "7--15",
editor = "Alexander Ivrii and Ofer Strichman and Hunt, {Warren A.} and Georg Weissenbacher",
booktitle = "Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design, FMCAD 2020",
publisher = "Institute of Electrical and Electronics Engineers",
address = "United States",
}