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!
cited_by
cites cdi_FETCH-LOGICAL-c991-413ea8f093da4386e280a6a02062252e1f4f3cc0fa989b58da8c3ddea754e5333
container_end_page 18
container_issue 1
container_start_page 4
container_title International journal on software tools for technology transfer
container_volume 7
creator BRABERMAN, Victor
OLIVERO, Alfredo
SCHAPACHNIK, Fernando
description 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]
doi_str_mv 10.1007/s10009-004-0143-z
format article
fullrecord <record><control><sourceid>proquest_cross</sourceid><recordid>TN_cdi_proquest_journals_197473261</recordid><sourceformat>XML</sourceformat><sourcesystem>PC</sourcesystem><sourcerecordid>788255091</sourcerecordid><originalsourceid>FETCH-LOGICAL-c991-413ea8f093da4386e280a6a02062252e1f4f3cc0fa989b58da8c3ddea754e5333</originalsourceid><addsrcrecordid>eNpFULlOAzEUtBBIhOMD6FZIlIbntdcHHUQckSLRpKKxHB_gsNkN9m5Bvh5HiaCZmWJm3tMgdEXglgCIu1wQFAZgGAijeHuEJoUproUUx39aqFN0lvMKgAgu1ASpWc6jz1XsKhfzkOJyHLyrhrguuO6dbyv76e1X7D7uq8cxtq6o6t2P-QKdBNNmf3ngc7R4flpMX_H87WU2fZhjqxTBjFBvZABFnWFUcl9LMNxADbyum9qTwAK1FoJRUi0b6Yy01DlvRMN8Qyk9R9f72k3qv8ung171Y-rKRU2UYILWnBQT2Zts6nNOPuhNimuTfjQBvdtH7_fRZR-920dvS-bmUGyyNW1IprMx_wd5IzhrBP0FQitkZg</addsrcrecordid><sourcetype>Aggregation Database</sourcetype><iscdi>true</iscdi><recordtype>article</recordtype><pqid>197473261</pqid></control><display><type>article</type><title>Issues in distributed timed model checking: Building Zeus</title><source>Springer Nature</source><creator>BRABERMAN, Victor ; OLIVERO, Alfredo ; SCHAPACHNIK, Fernando</creator><creatorcontrib>BRABERMAN, Victor ; OLIVERO, Alfredo ; SCHAPACHNIK, Fernando</creatorcontrib><description>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]</description><identifier>ISSN: 1433-2779</identifier><identifier>EISSN: 1433-2787</identifier><identifier>DOI: 10.1007/s10009-004-0143-z</identifier><language>eng</language><publisher>Berlin: Springer</publisher><subject>Applied sciences ; Computer science; control theory; systems ; Computer systems and distributed systems. User interface ; Distributed control systems ; Exact sciences and technology ; Software</subject><ispartof>International journal on software tools for technology transfer, 2005-02, Vol.7 (1), p.4-18</ispartof><rights>2005 INIST-CNRS</rights><rights>Springer-Verlag 2005</rights><lds50>peer_reviewed</lds50><woscitedreferencessubscribed>false</woscitedreferencessubscribed><cites>FETCH-LOGICAL-c991-413ea8f093da4386e280a6a02062252e1f4f3cc0fa989b58da8c3ddea754e5333</cites></display><links><openurl>$$Topenurl_article</openurl><openurlfulltext>$$Topenurlfull_article</openurlfulltext><thumbnail>$$Tsyndetics_thumb_exl</thumbnail><link.rule.ids>309,310,314,780,784,789,790,23930,23931,25140,27924,27925</link.rule.ids><backlink>$$Uhttp://pascal-francis.inist.fr/vibad/index.php?action=getRecordDetail&amp;idt=16576457$$DView record in Pascal Francis$$Hfree_for_read</backlink></links><search><creatorcontrib>BRABERMAN, Victor</creatorcontrib><creatorcontrib>OLIVERO, Alfredo</creatorcontrib><creatorcontrib>SCHAPACHNIK, Fernando</creatorcontrib><title>Issues in distributed timed model checking: Building Zeus</title><title>International journal on software tools for technology transfer</title><description>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]</description><subject>Applied sciences</subject><subject>Computer science; control theory; systems</subject><subject>Computer systems and distributed systems. User interface</subject><subject>Distributed control systems</subject><subject>Exact sciences and technology</subject><subject>Software</subject><issn>1433-2779</issn><issn>1433-2787</issn><fulltext>true</fulltext><rsrctype>article</rsrctype><creationdate>2005</creationdate><recordtype>article</recordtype><recordid>eNpFULlOAzEUtBBIhOMD6FZIlIbntdcHHUQckSLRpKKxHB_gsNkN9m5Bvh5HiaCZmWJm3tMgdEXglgCIu1wQFAZgGAijeHuEJoUproUUx39aqFN0lvMKgAgu1ASpWc6jz1XsKhfzkOJyHLyrhrguuO6dbyv76e1X7D7uq8cxtq6o6t2P-QKdBNNmf3ngc7R4flpMX_H87WU2fZhjqxTBjFBvZABFnWFUcl9LMNxADbyum9qTwAK1FoJRUi0b6Yy01DlvRMN8Qyk9R9f72k3qv8ung171Y-rKRU2UYILWnBQT2Zts6nNOPuhNimuTfjQBvdtH7_fRZR-920dvS-bmUGyyNW1IprMx_wd5IzhrBP0FQitkZg</recordid><startdate>20050201</startdate><enddate>20050201</enddate><creator>BRABERMAN, Victor</creator><creator>OLIVERO, Alfredo</creator><creator>SCHAPACHNIK, Fernando</creator><general>Springer</general><general>Springer Nature B.V</general><scope>IQODW</scope><scope>AAYXX</scope><scope>CITATION</scope><scope>3V.</scope><scope>7SC</scope><scope>7XB</scope><scope>8AL</scope><scope>8AO</scope><scope>8FD</scope><scope>8FE</scope><scope>8FG</scope><scope>8FK</scope><scope>8G5</scope><scope>ABJCF</scope><scope>ABUWG</scope><scope>AFKRA</scope><scope>ARAPS</scope><scope>AZQEC</scope><scope>BENPR</scope><scope>BGLVJ</scope><scope>CCPQU</scope><scope>DWQXO</scope><scope>GNUQQ</scope><scope>GUQSH</scope><scope>HCIFZ</scope><scope>JQ2</scope><scope>K7-</scope><scope>L6V</scope><scope>L7M</scope><scope>L~C</scope><scope>L~D</scope><scope>M0N</scope><scope>M2O</scope><scope>M7S</scope><scope>MBDVC</scope><scope>P5Z</scope><scope>P62</scope><scope>PADUT</scope><scope>PQEST</scope><scope>PQQKQ</scope><scope>PQUKI</scope><scope>PRINS</scope><scope>PTHSS</scope><scope>Q9U</scope></search><sort><creationdate>20050201</creationdate><title>Issues in distributed timed model checking: Building Zeus</title><author>BRABERMAN, Victor ; OLIVERO, Alfredo ; SCHAPACHNIK, Fernando</author></sort><facets><frbrtype>5</frbrtype><frbrgroupid>cdi_FETCH-LOGICAL-c991-413ea8f093da4386e280a6a02062252e1f4f3cc0fa989b58da8c3ddea754e5333</frbrgroupid><rsrctype>articles</rsrctype><prefilter>articles</prefilter><language>eng</language><creationdate>2005</creationdate><topic>Applied sciences</topic><topic>Computer science; control theory; systems</topic><topic>Computer systems and distributed systems. User interface</topic><topic>Distributed control systems</topic><topic>Exact sciences and technology</topic><topic>Software</topic><toplevel>peer_reviewed</toplevel><toplevel>online_resources</toplevel><creatorcontrib>BRABERMAN, Victor</creatorcontrib><creatorcontrib>OLIVERO, Alfredo</creatorcontrib><creatorcontrib>SCHAPACHNIK, Fernando</creatorcontrib><collection>Pascal-Francis</collection><collection>CrossRef</collection><collection>ProQuest Central (Corporate)</collection><collection>Computer and Information Systems Abstracts</collection><collection>ProQuest Central (purchase pre-March 2016)</collection><collection>Computing Database (Alumni Edition)</collection><collection>ProQuest Pharma Collection</collection><collection>Technology Research Database</collection><collection>ProQuest SciTech Collection</collection><collection>ProQuest Technology Collection</collection><collection>ProQuest Central (Alumni) (purchase pre-March 2016)</collection><collection>Research Library (Alumni Edition)</collection><collection>Materials Science &amp; Engineering Collection</collection><collection>ProQuest Central (Alumni Edition)</collection><collection>ProQuest Central</collection><collection>Advanced Technologies &amp; Aerospace Collection</collection><collection>ProQuest Central Essentials</collection><collection>ProQuest Central</collection><collection>Technology Collection</collection><collection>ProQuest One Community College</collection><collection>ProQuest Central</collection><collection>ProQuest Central Student</collection><collection>Research Library Prep</collection><collection>SciTech Premium Collection</collection><collection>ProQuest Computer Science Collection</collection><collection>Computer Science Database</collection><collection>ProQuest Engineering Collection</collection><collection>Advanced Technologies Database with Aerospace</collection><collection>Computer and Information Systems Abstracts – Academic</collection><collection>Computer and Information Systems Abstracts Professional</collection><collection>Computing Database</collection><collection>Research Library</collection><collection>Engineering Database</collection><collection>Research Library (Corporate)</collection><collection>Advanced Technologies &amp; Aerospace Database</collection><collection>ProQuest Advanced Technologies &amp; Aerospace Collection</collection><collection>Research Library China</collection><collection>ProQuest One Academic Eastern Edition (DO NOT USE)</collection><collection>ProQuest One Academic</collection><collection>ProQuest One Academic UKI Edition</collection><collection>ProQuest Central China</collection><collection>Engineering Collection</collection><collection>ProQuest Central Basic</collection><jtitle>International journal on software tools for technology transfer</jtitle></facets><delivery><delcategory>Remote Search Resource</delcategory><fulltext>fulltext</fulltext></delivery><addata><au>BRABERMAN, Victor</au><au>OLIVERO, Alfredo</au><au>SCHAPACHNIK, Fernando</au><format>journal</format><genre>article</genre><ristype>JOUR</ristype><atitle>Issues in distributed timed model checking: Building Zeus</atitle><jtitle>International journal on software tools for technology transfer</jtitle><date>2005-02-01</date><risdate>2005</risdate><volume>7</volume><issue>1</issue><spage>4</spage><epage>18</epage><pages>4-18</pages><issn>1433-2779</issn><eissn>1433-2787</eissn><abstract>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]</abstract><cop>Berlin</cop><pub>Springer</pub><doi>10.1007/s10009-004-0143-z</doi><tpages>15</tpages></addata></record>
fulltext fulltext
identifier ISSN: 1433-2779
ispartof International journal on software tools for technology transfer, 2005-02, Vol.7 (1), p.4-18
issn 1433-2779
1433-2787
language eng
recordid cdi_proquest_journals_197473261
source Springer Nature
subjects Applied sciences
Computer science
control theory
systems
Computer systems and distributed systems. User interface
Distributed control systems
Exact sciences and technology
Software
title Issues in distributed timed model checking: Building Zeus
url http://sfxeu10.hosted.exlibrisgroup.com/loughborough?ctx_ver=Z39.88-2004&ctx_enc=info:ofi/enc:UTF-8&ctx_tim=2024-12-26T14%3A44%3A48IST&url_ver=Z39.88-2004&url_ctx_fmt=infofi/fmt:kev:mtx:ctx&rfr_id=info:sid/primo.exlibrisgroup.com:primo3-Article-proquest_cross&rft_val_fmt=info:ofi/fmt:kev:mtx:journal&rft.genre=article&rft.atitle=Issues%20in%20distributed%20timed%20model%20checking:%20Building%20Zeus&rft.jtitle=International%20journal%20on%20software%20tools%20for%20technology%20transfer&rft.au=BRABERMAN,%20Victor&rft.date=2005-02-01&rft.volume=7&rft.issue=1&rft.spage=4&rft.epage=18&rft.pages=4-18&rft.issn=1433-2779&rft.eissn=1433-2787&rft_id=info:doi/10.1007/s10009-004-0143-z&rft_dat=%3Cproquest_cross%3E788255091%3C/proquest_cross%3E%3Cgrp_id%3Ecdi_FETCH-LOGICAL-c991-413ea8f093da4386e280a6a02062252e1f4f3cc0fa989b58da8c3ddea754e5333%3C/grp_id%3E%3Coa%3E%3C/oa%3E%3Curl%3E%3C/url%3E&rft_id=info:oai/&rft_pqid=197473261&rft_id=info:pmid/&rfr_iscdi=true