Proposition of an Action Layer for Electrum

Abstract

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 (\textsf {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.

Document

If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.

Reference

% BibTex
@inproceedings{BrunelCCHMT18,
  author       = {Julien Brunel and
                  David Chemouil and
                  Alcino Cunha and
                  Thomas Hujsa and
                  Nuno Macedo and
                  Jeanne Tawa},
  editor       = {Michael J. Butler and
                  Alexander Raschke and
                  Thai Son Hoang and
                  Klaus Reichl},
  title        = {Proposition of an Action Layer for Electrum},
  booktitle    = {Abstract State Machines, Alloy, B, TLA, VDM, and {Z} - 6th International
                  Conference, {ABZ} 2018, Southampton, UK, June 5-8, 2018, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {10817},
  pages        = {397--402},
  publisher    = {Springer},
  year         = {2018},
  url          = {https://doi.org/10.1007/978-3-319-91271-4\_30},
  doi          = {10.1007/978-3-319-91271-4\_30},
  timestamp    = {Tue, 25 Jun 2024 21:03:18 +0200},
  biburl       = {https://dblp.org/rec/conf/asm/BrunelCCHMT18.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}