An abstraction technique for parameterized model checking of leader election protocols: application to FTSP

DOI10.1007/978-3-662-54577-5_2MaRDI QIDQ3303889zbMATH OpenOpenAlexFDO

Authors Ocan Sankur, Jean-Pierre Talpin

Publication date 5 August 2020

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-662-54577-5_2

Mathematics Subject Classification ID

Network protocols (68M12) Distributed systems (68M14) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Parameterized model checking of synchronous distributed algorithms by abstraction
• Verification of an industrial asynchronous leader election algorithm using abstractions and parametric model checking
• Parameterized model checking of networks of timed automata with Boolean guards
• Parameterized verification of leader/follower systems via first-order temporal logic
• But what if I don't want to wait forever?

Cites work

• A calculus of communicating systems
• A theory of timed automata
• An improved algorithm for decentralized extrema-finding in circular configurations of processes
• An O(n log n) unidirectional distributed algorithm for extrema finding in a circle
• Formal Methods in Computer-Aided Design
• Formal verification of a leader election protocol in process algebra
• scientific article; zbMATH DE number 1852158 (Why is no real title available?)
• scientific article; zbMATH DE number 1903348 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• Parameterized verification of broadcast networks of register automata
• Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems

Cited in

(4)

• Verification of an industrial asynchronous leader election algorithm using abstractions and parametric model checking
• scientific article; zbMATH DE number 2081106 (Why is no real title available?)
• Timed automata verification and synthesis via finite automata learning
• Timed automata verification and synthesis via finite automata learning

This page was built for publication: An abstraction technique for parameterized model checking of leader election protocols: application to FTSP

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