Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/89470| Título: | Quantitative relational modelling with QAlloy |
| Autor(es): | Silva, Pedro Oliveira, José Nuno Fonseca Macedo, Nuno Cunha, Alcino |
| Palavras-chave: | Alloy linear algebra model finding quantitative modelling relational specifications SMT |
| Data: | 2022 |
| Editora: | ACM |
| Citação: | Silva, P., Oliveira, J. N., Macedo, N., & Cunha, A. (2022, November 7). Quantitative relational modelling with QAlloy. Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering. ACM. http://doi.org/10.1145/3540250.3549154 |
| Resumo(s): | Alloy is a popular language and tool for formal software design. A key factor to this popularity is its relational logic, an elegant specification language with a minimal syntax and semantics. However, many software problems nowadays involve both structural and quantitative requirements, and Alloy's relational logic is not well suited to reason about the latter. This paper introduces QAlloy, an extension of Alloy with quantitative relations that add integer quantities to associations between domain elements. Having integers internalised in relations, instead of being explicit domain elements like in standard Alloy, allows quantitative requirements to be specified in QAlloy with a similar elegance to structural requirements, with the side-effect of providing basic dimensional analysis support via the type system. The QAlloy Analyzer also implements an SMT-based engine that enables quantities to be unbounded, thus avoiding many problems that may arise with the current bounded integer semantics of Alloy. |
| Tipo: | Artigo em ata de conferência |
| URI: | https://hdl.handle.net/1822/89470 |
| ISBN: | 9781450394130 |
| DOI: | 10.1145/3540250.3549154 |
| Versão da editora: | https://dl.acm.org/doi/10.1145/3540250.3549154 |
| Arbitragem científica: | yes |
| Acesso: | Acesso aberto |
| Aparece nas coleções: |
