Proposition of an Action Layer for Electrum

• Type: Article in International Conference Proceedings Book
• Date: 2018

Authors

Brunel, J (Author) Other; Chemouil, D (Author) Other; Cunha, A (Author) Other; Hujsa, T (Author) Other; Macedo, N (Author) Other; Tawa, J (Author) Other

Conference proceedings International

Title: Abstract State Machines, Alloy, B, TLA, VDM, and Z - 6th International Conference, ABZ 2018, Southampton, UK, June 5-8, 2018, Proceedings

Pages: 397-402

6th International Conference on ABZ Conference on ASM, Alloy, B, TLA, VDM, and Z, ABZ 2018

5 June 2018 through 8 June 2018

Indexing

Scopus - 2 Citations

Other information

Authenticus ID: P-00N-YKZ

DOI: 10.1007/978-3-319-91271-4_30

Abstract (EN): Electrum is an extension of Alloy that adds (1) mutable signatures and fields to the modeling layer; and (2) connectives from linear temporal logic (with past) and primed variables à la TLA+ to the constraint language. The analysis of models can then be translated into a SAT-based bounded model-checking problem, or to an LTL-based unbounded model-checking problem. Electrum has proved to be useful to model and verify dynamic systems with rich configurations. However, when specifying events, the tedious and sometimes error-prone handling of traces and frame conditions (similarly as in Alloy) remained necessary. In this paper, we introduce an extension of Electrum with a so-called ¿action¿ layer that addresses these questions. © Springer International Publishing AG, part of Springer Nature 2018.

Language: English

Type (Professor's evaluation): Scientific