Verification of an industrial asynchronous leader election algorithm using abstractions and parametric model checking

DOI10.1007/978-3-030-11245-5_19MaRDI QIDQ2287101zbMATH OpenOpenAlexFDO

Authors Étienne André, Laurent Fribourg, Jean-Marc Mota, Romain Soulat

Publication date 23 January 2020

Full work available at URL https://arxiv.org/abs/1812.08949

zbMATH Keywords

model checkingdistributed algorithmleader electionparametric timed automataparameterized verificationsaveprover

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 2081106
• An abstraction technique for parameterized model checking of leader election protocols: application to FTSP
• Formal verification of a leader election protocol in process algebra
• Parameterized verification of leader/follower systems via first-order temporal logic
• scientific article; zbMATH DE number 1444728

Cited in

(8)

• An abstraction technique for parameterized model checking of leader election protocols: application to FTSP
• scientific article; zbMATH DE number 7577576 (Why is no real title available?)
• \textsf{IMITATOR} 3: synthesis of timing parameters beyond decidability
• Parametric schedulability analysis of a launcher flight control system under reactivity constraints
• Timed automata relaxation for reachability
• Cycle encoding-based parameter synthesis for timed automata safety
• scientific article; zbMATH DE number 2081106 (Why is no real title available?)
• A timed verification of the IEEE 1394 Leader election protocol

This page was built for publication: Verification of an industrial asynchronous leader election algorithm using abstractions and parametric model checking

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