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.)
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 electrum-2.1.5.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 electrum-2.1.5.jar --help
To perform analyses on an unbounded time horizon, one needs to have installed Electrod program, as well as NuSMV or nuXmv. (REMARK: since version 2.1.2, Electrod is directly shipped inside the Electrum Analyzer; NuSMV and nuXmv must still be retrieved separately.)
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 proposal.
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, can be found here. Or access directly the:
- Electrum model and theme
- Alloy model and theme
- Conference paper and extended version describing its development
ELS Case Study
Our response to the ABZ 2020 call for case study submissions, the ELS, can be found here. Or access directly the:
- Single variant Electrum models, EU, USA, EU+Armored and USA+Armored
- Pure Electrum SPL model
- Colorful Electrum SPL model
- The theme for all the models above
- Accepted paper describing its development
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
- Nuno Macedo, HASLab, INESC TEC & Universidade do Porto, Portugal
- Julien Brunel, ONERA/DTIS & Université fédérale de Toulouse, France
- David Chemouil, ONERA/DTIS & Université fédérale de Toulouse, France
- Alcino Cunha, HASLab, INESC TEC & Universidade do Minho, Portugal
- Denis Kuperberg, TU Munich, Germany
- Eduardo Pessoa, HASLab, INESC TEC & Universidade do Minho, Portugal
History
Electrum 2.1 (November 2020)
- Slight changes to the language
- Trace visualizer with additional exploration operations
- Several interface/reporting improvements
Electrum 2.0 (October 2019)
- Rebased to Alloy Analyzer 5
- Slight changes to the language
- Trace visualizer with additional exploration operations
Electrum 1.2 (April 2019)
- Several improvements and bug fixes to the interface, visualiser and evaluator
Electrum 1.1 (May 2018)
- Initial support for symbolic bound extraction
- Repository of examples
- Many enhancements and bug fixes
- Accompanied the ASE’18 submission
Electrum 1.0 (January 2018)
- First stable public release (accompanying the ABZ’18 submission)
- Common interface for temporal relational model finding problems through Pardinus
- Bounded and unbounded model checking of Electrum models
- Uniform visualization of trace instances
- Support for a decomposed solving strategy
Electrum 0.2 (November 2016)
- Direct embedding into a temporal extension to Kodkod (Pardinus)
- Visualizer natively supports temporal solutions
Electrum 0.1 (March 2016)
- First release (accompanying the FSE’16 submission)
- Bounded model checking of Electrum models
- Electrum models expanded into Alloy models
- Expanded Alloy models returned to the visualizer
Publications
Electrum has been developed in the context of the TRUST project, and incorporates contributions from several publications:
- J. Brunel, D. Chemouil, A. Cunha and N. Macedo. The Electrum Analyzer: Model checking relational first-order temporal specifications. In the proceedings ASE’18. ACM, 2018.
- A. Cunha and N. Macedo. Validating the Hybrid ERTMS/ETCS Level 3 concept with Electrum. In the proceedings of ABZ’18. LNCS 10817. Springer, 2018.
- J. Brunel, D. Chemouil, A. Cunha, T. Hujsa, N. Macedo and J. Tawa. Proposition of an action layer for Electrum. In the proceedings of ABZ’18. LNCS 10817. Springer, 2018.
- N. Macedo, A. Cunha and E. Pessoa. Exploiting partial knowledge for efficient model analysis. In the proceedings of ATVA’17. LNCS 10482. Springer, 2017.
- N. Macedo, J. Brunel, D. Chemouil, A. Cunha and D. Kuperberg. Lightweight specification and analysis of dynamic systems with rich configurations. In the proceedings of FSE’16. ACM, 2016.
- N. Macedo, A. Cunha and T. Guimarães. Exploring scenario exploration. In the proceedings of FASE’15. LNCS 9033. Springer, 2015.
- A. Cunha, N. Macedo and T. Guimarães. Target oriented relational model finding. In the proceedings of FASE’14. LNCS 8411. Springer, 2014.
This work is financed by the ERDF – European Regional Development Fund through the Operational Programme for Competitiveness and Internationalisation - COMPETE 2020 Programme and by National Funds through the Portuguese funding agency, FCT - Fundação para a Ciência e a Tecnologia, within project POCI-01-0145-FEDER-016826.
