Issues in distributed timed model checking

被引：4

作者：

Braberman V. ^{[1
]}

Olivero A. ^{[2
]}

Schapachnik F. ^{[1
]}

机构：

[1] Computer Science Department, FCEyN, Universidad de Buenos Aires, Buenos Aires

[2] Department of Information Technology, FIyCE, Universidad Argentina de la Empresa, Buenos Aires

来源：

International Journal on Software Tools for Technology Transfer | 2005年 / 7卷 / 1期

关键词：

Distributed timed model checking; KRONOS; Timed automata; Timed systems; ZEUS;

D O I：

10.1007/s10009-004-0143-z

中图分类号：

学科分类号：

摘要：

In this work we present ZEUS, a distributed timed model checker that evolves from the TCTL model checker Kronos [13] and that currently can handle backwards computation of reachability properties [2] over timed automata [3]. ZEUS was developed following a software architecture-centric approach. Its conceptual architecture was conceived to be sufficiently modular to house several features such as a priori graph partitioning, synchronous and asynchronous computation, communication piggybacking, delayed messaging, and dead-time utilization. Surprisingly enough, early experiments pinpointed the difficulties of getting speedups using asynchronous versions and showed interesting results on the synchronous counterpart, although being intuitively less attractive. © Springer-Verlag 2004.

引用

页码：4 / 18

页数：14