Dealing with practical limitations of distributed timed model checking for timed automata

DOI10.1007/S10703-006-0012-3zbMATH Open1110.68073OpenAlexW2004173170MaRDI QIDQ2431767FDOQ2431767

Authors: V. Braberman, A. Olivero, F. Schapachnik 

Publication date: 24 October 2006

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-006-0012-3

Recommendations

• \textsc{Zeus}: a distributed timed model-checker based on \textsc{Kronos}
• On-the-fly workload prediction and redistribution in the distributed timed model checker Zeus
• scientific article; zbMATH DE number 1670779
• Multi-core Reachability for Timed Automata
• Formal Modeling and Analysis of Timed Systems

zbMATH Keywords

ReachabilityTimed automataRedistributionReconfigurationDBMDistributed timed model checkingLoad-balance

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Cites Work

• A theory of timed automata
• Model-checking in dense real-time
• Symbolic model checking for real-time systems
• On-the-fly workload prediction and redistribution in the distributed timed model checker Zeus
• Computer Aided Verification
• Title not available (Why is that?)
• A scalable parallel algorithm for reachability analysis of very large circuits
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Dealing with practical limitations of distributed timed model checking for timed automata
• \textsc{Zeus}: a distributed timed model-checker based on \textsc{Kronos}
• Title not available (Why is that?)

Cited In (6)

• Dealing with practical limitations of distributed timed model checking for timed automata
• Title not available (Why is that?)
• \textsc{Zeus}: a distributed timed model-checker based on \textsc{Kronos}
• Timed Multiset Rewriting and the Verification of Time-Sensitive Distributed Systems
• On-the-fly workload prediction and redistribution in the distributed timed model checker Zeus
• Bounded model checking distributed temporal logic

Uses Software

• Kronos
• Uppaal

This page was built for publication: Dealing with practical limitations of distributed timed model checking for timed automata

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2431767)