Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/68518
Título: | Proposition of an action layer for electrum |
Autor(es): | Brunel, Julien Chemouil, David Cunha, Alcino Hujsa, Thomas Macedo, Nuno Tawa, Jeanne |
Data: | 2018 |
Editora: | Springer Verlag |
Revista: | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
Resumo(s): | 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. |
Tipo: | Artigo em ata de conferência |
URI: | https://hdl.handle.net/1822/68518 |
ISBN: | 9783319912707 |
DOI: | 10.1007/978-3-319-91271-4_30 |
ISSN: | 0302-9743 |
Versão da editora: | https://link.springer.com/chapter/10.1007%2F978-3-319-91271-4_30 |
Arbitragem científica: | yes |
Acesso: | Acesso aberto |
Aparece nas coleções: |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
abz18short.pdf | 297,64 kB | Adobe PDF | Ver/Abrir |