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.
Wed 16 NovDisplayed time zone: Beijing, Chongqing, Hong Kong, Urumqi change
14:00 - 15:30 | DependabilityIndustry Paper / Research Papers at SRC LT 51 Chair(s): Tao Yue Simula Research Laboratory | ||
14:00 15mTalk | Unite: An Adapter for Transforming Analysis Tools to Web Services via OSLC Industry Paper Ondřej Vašíček Brno University of Technology; Honeywell International, Jan Fiedor Brno University of Technology; Honeywell International, Tomáš Kratochvíla Honeywell International, Bohuslav Křena Brno University of Technology, Aleš Smrčka Brno University of Technology, Tomáš Vojnar Brno University of Technology DOI | ||
14:15 15mTalk | Discovering Feature Flag Interdependencies in Microsoft Office Industry Paper Michael Schröder TU Wien, Katja Kevic Microsoft, Dan Gopstein Microsoft, Brendan Murphy Microsoft, Jennifer Beckmann Microsoft DOI Pre-print Media Attached | ||
14:30 15mTalk | Demystifying the Underground Ecosystem of Account Registration Bots Research Papers Yuhao Gao University of Technology Sydney; Beijing University of Posts and Telecommunications, Guoai Xu Harbin Institute of Technology; Beijing University of Posts and Telecommunications, Li Li Monash University, Xiapu Luo Hong Kong Polytechnic University, Chenyu Wang Beijing University of Posts and Telecommunications, Yulei Sui University of New South Wales DOI | ||
14:45 15mResearch paper | Quantitative Relational Modelling with QAlloy Research Papers Pedro Silva University of Minho; INESC TEC, Jose Nuno Oliveira University of Minho; INESC TEC, Nuno Macedo University of Porto; INESC TEC, Alcino Cunha University of Minho; INESC TEC DOI Pre-print | ||
15:00 15mTalk | Using Graph Neural Networks for Program Termination Research Papers DOI |