Issues in distributed timed model checking: Building Zeus

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...

Full description

Saved in:
Bibliographic Details
Published in:International journal on software tools for technology transfer 2005-02, Vol.7 (1), p.4-18
Main Authors: BRABERMAN, Victor, OLIVERO, Alfredo, SCHAPACHNIK, Fernando
Format: Article
Language:English
Subjects:
Applied sciences
Computer science
control theory
systems
Computer systems and distributed systems. User interface
Distributed control systems
Exact sciences and technology
Software
Citations: Items that this one cites
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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. [PUBLICATION ABSTRACT]
ISSN:1433-2779
1433-2787
DOI:10.1007/s10009-004-0143-z