Proposition of an Action Layer for Electrum
Proposition of an Action Layer for Electrum
复制标题
提出 Electrum 行动层
DOI：
--
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Jeanne Tawa
中科院分区：
文献类型：
--
作者：
Julien Brunel;D. Chemouil;Alcino Cunha;Thomas Hujsa;Nuno Macedo;Jeanne Tawa
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 a la ( extsf {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.
