PV4 ⊧ Consensus Verifiertranslates a consensus algorithm into a PROMELA model and LTL properties

Model checking tool for consensus algorithms formulated in the ConsL language

Application domain/field

• Consensus algorithms
• Fault-tolerant distributed systems

Type of tool

Specification/model translator?

Expected input

Consensus algorithm

Format:

ConsL (own) language

Expected output

PROMELA/Spin model

Internals

The tool automatically translates a ConsL algorithm into appropriate PROMELA models and LTL properties for the SPIN model checker.