文章基本信息

标题：Model checking time-constrained scenario-based specifications
本地全文：下载
作者：S. Akshay ; Paul Gastin ; Madhavan Mukund 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2010
卷号：8
页码：204-215
DOI：10.4230/LIPIcs.FSTTCS.2010.204
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：We consider the problem of model checking message-passing systems with real-time requirements. As behavioural specifications, we use message sequence charts (MSCs) annotated with timing constraints. Our system model is a network of communicating finite state machines with local clocks, whose global behaviour can be regarded as a timed automaton. Our goal is to verify that all timed behaviours exhibited by the system conform to the timing constraints imposed by the specification. In general, this corresponds to checking inclusion for timed languages, which is an undecidable problem even for timed regular languages. However, we show that we can translate regular collections of time-constrained MSCs into a special class of event-clock automata that can be determinized and complemented, thus permitting an algorithmic solution to the model checking problem.
关键词：model-checking; message-passing system; time-constrained MSC