Electrum is an extension to the Alloy Analyzer by INESC TEC (the Institute for Systems and Computer Engineering, Technology and Science) and ONERA (the French aerospace research center) provides an analyzer for Electrum models, a temporal extension to the Alloy modeling language. The Analyzer provides both bounded and unbounded model checking procedures.

Alloy is a simple structural modeling language based on first-order logic developed at the Software Design Group. Its Analyzer can generate instances of invariants, simulate the execution of operations, and check user-specified properties of a model.

Getting started

The best way to get started with Electrum is to download the executable jar (see Running) and follow the tutorial. You can also watch the following video for an overview. (The video was recorded for Electrum 1, so there may be slight changes on the interface.)

Electrum Video

A repository of examples, including familiar Alloy examples converted into Electrum, is also available here.

Running

Download the executable jar and launch it simply as

$ java -jar electrum2.0.jar

This will launch Electrum’s/Alloy Analyzer’s simple GUI, which is packaged with several examples. The file can also by run from the command-line, for more information run

$ java -jar electrum2.0.jar --help

To perform analyses on an unbounded time horizon, one needs to have installed Electrod program, as well as NuSMV or nuXmv.

Building Electrum Analyzer

The Electrum Analyzer 2 inherits the building instructions from Alloy Analyzer 5.

Prototype: Electrum with actions

An extension of Electrum 1, with actions, is currently under study. Check out the paper with the preliminary proposition.

If you wish to build it, follow the building steps for Electrum 1, just replacing -b master in the first line by -b actions.

ERTMS Case Study

Our response to the ABZ 2018 call for case study submissions, the ERTMS system, can be found here. Or access directly the:

License

Electrum is open-source and available under the MIT license, as is the Alloy Analyzer. However, it utilizes several third-party packages whose code may be distributed under a different license (see the various LICENSE files in the distribution for details), including Kodod and its extension Pardinus, and the underlying solvers (SAT4J, MiniSat, Glucose/Syrup, (P)Lingeling, Yices, zChaff, CryptoMiniSat and Electrod. CUP and JFlex are also used to generate the parser.

Collaborators

History

Electrum 2.0 (October 2019)

Electrum 1.2 (April 2019)

Electrum 1.1 (May 2018)

Electrum 1.0 (January 2018)

Electrum 0.2 (November 2016)

Electrum 0.1 (March 2016)

Publications

Electrum has been developed in the context of the TRUST project, and incorporates contributions from several publications: