Proposition of an Action Layer for Electrum

• Tipo: Artigo em Livro de Atas de Conferência Internacional
• Data: 2018

Autores

Brunel, J (Autor) Outra; Chemouil, D (Autor) Outra; Cunha, A (Autor) Outra; Hujsa, T (Autor) Outra; Macedo, N (Autor) Outra; Tawa, J (Autor) Outra

Ata de Conferência Internacional

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

Páginas: 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

Indexação

Scopus - 2 Citações

Outras Informações

ID Authenticus: 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.

Idioma: Inglês

Tipo (Avaliação Docente): Científica