PV4 ⊧ Electrum Analyzer (sometimes called 'Electrum')checks assertions and LTL properties in Electrum models with bounded or unbounded model checking

Model checker for Electrum specifications

Application domain/field

• Model checking
• Relational logic
• Relational specifications

Type of tool

Model checker

Expected input

• Electrum model
• Optional: assertions (LTL properties)

Format:

Electrum language

Internals

Electrum is an extension of Alloy that enriches its relational logic with LTL operators. The Electrum Analyzer can do bounded model checking (encoded into SAT) and unbounded model checking (encoding into SMV) There are two main commands to analyse Electrum models:

• run: searches for instances that satisfy certain properties
• check: searches for counter-examples that break desirable properties

There is a visualiser to inspect the results of the run and check commands.

Comments

License: Apache License 2.0