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

DOI10.1007/978-3-030-11245-5_19OpenAlexW2906360881MaRDI QIDQ2287101FDOQ2287101

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

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

zbMATH Keywords

model checkingdistributed algorithmleader electionparametric timed automataparameterized verificationsaveprover

Mathematics Subject Classification ID

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

Cited In (8)

• \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
• Title not available (Why is that?)
• A timed verification of the IEEE 1394 Leader election protocol
• An abstraction technique for parameterized model checking of leader election protocols: application to FTSP
• Title not available (Why is that?)

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)