kirancodes.me
To Proof Maintenance & Beyond!
FSE 2022

Quantitative relational modelling with QAlloy

Pedro Silva, José N. Oliveira, Nuno Macedo, Alcino Cunha

Full textDOI 10.1145/3540250.3549154dblp

Abstract

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.

BibTeX
@inproceedings{Silva-al:FSE22,
  author    = {Pedro Silva and
               Jos{\'{e}} N. Oliveira and
               Nuno Macedo and
               Alcino Cunha},
  title     = {Quantitative relational modelling with {QAlloy}},
  booktitle = {{ESEC/SIGSOFT} {FSE}},
  pages     = {885--896},
  publisher = {{ACM}},
  year      = {2022},
}

Related papers