文章基本信息

标题：Diagnostic Model Checking for Real-Time Systems
本地全文：下载
作者：Kim G. Larsen ; Paul Pettersson ; Wang Yi 等
期刊名称：BRICS Report Series
印刷版ISSN：0909-0878
出版年度：1996
卷号：3
期号：57
出版社：Aarhus University
摘要：Uppaal is a new tool suit for automatic verification of networks of timed automata. In this paper we describe the diagnostic model-checking feature of Uppaal and illustrates its usefulness through the debugging of (a version of) the Philips Audio-Control Protocol. Together with a graphical interface of Uppaal this diagnostic feature allows for a number of errors to be more easily detected and corrected.