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
相关论文
共 31 条
  • [1] Alur R., Courcoubetis C., Dill D., Halbwachs N., Wong-Toi H., An implementation of three algorithms for timing verification based on automata emptiness, Proceedings of the 13th IEEE Real-Time Systems Symposium (RTSS '92), pp. 157-166, (1992)
  • [2] Alur R., Courcoubetis C., Dill D.L., Model-checking in dense real-time, Inf. Comput., 104, 1, pp. 2-34, (1993)
  • [3] Alur R., Dill D.L., A theory of timed automata, Theor. Comput. Sci., 126, 2, pp. 183-235, (1994)
  • [4] Barnat J., Brim L., Stribrna J., Distributed LTL model-checking in SPIN, Proceedings of the 7th International SPIN Workshop, 2057, pp. 200-216, (2001)
  • [5] Behrmann G., A performance study of distributed timed automata reachability analysis, Proceedings of the Workshop on Parallel and Distributed Model Checking, Affiliated With the 13th International Conference on Concurrency Theory (CONCUR '02), 68, (2002)
  • [6] Behrmann G., Hune T., Vaandrager F.W., Distributing timed model checking how the search order matters, Proceedings of the 12th International Conference on Computer Aided Verification (CAV '00), 1855, pp. 216-231, (2000)
  • [7] Ben-David S., Heyman T., Grumberg O., Schuster A., Scalable distributed on-the-fly symbolic model checking, Proceedings of the 3rd International Conference on Formal Methods in Computer-Aided Design 2000, 1954, pp. 390-404, (2000)
  • [8] Bollig B., Leucker M., Weber M., Parallel model checking for the alternation free μ-calculus, Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '01), 2031, pp. 543-558, (2001)
  • [9] Braberman V., Garbervetsky D., Olivero A., Improving the verification of timed systems using influence information, Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '02), 2280, pp. 21-36, (2002)
  • [10] Braberman V., Lopez Pombo C., Olivero A., On improving backwards verification for timed automata, Proceedings of the Workshop on Theory and Practice of Timed Systems (TPTS '02), 65, (2002)
1234