AlloyMax: Bringing Maximum Satisfaction to Relational SpecificationsDistinguished Paper Award

Fri 27 Aug 2021 23:00 - 23:10 - Architectures & Design—Model-Driven Software Engineering Chair(s): Davide Di Ruscio
Alloy is a declarative modeling language based on a first-order relational logic. Its constraint-based analysis has enabled a wide range of applications in software engineering, including configuration synthesis, bug finding, test-case generation, and security analysis. Certain types of analysis tasks in these domains involve finding an \emph{optimal} solution. For example, in a network configuration problem, instead of finding any valid configuration, it may be desirable to find one that is most \emph{permissive} (i.e., it permits a maximum number of packets). Due to its dependence on SAT, however, Alloy cannot be used to specify and analyze these types of problems.
We propose $\textnormal{Alloy}^{\textnormal{Max}}$, an extension of Alloy with a capability to express and analyze problems with optimal solutions. $\textnormal{Alloy}^{\textnormal{Max}}$ introduces (1) a small addition of language constructs that can be used to specify a wide range of problems that involve optimality and (2) a new analysis engine that leverages a \emph{Maximum Satisfiability} (\emph{MaxSAT}) solver to generate optimal solutions. To enable this new type of analysis, we show how a specification in a first-order relational logic can be translated into an input format of MaxSAT solvers—namely, a Boolean formula in \emph{weighted conjunctive normal form} (\emph{WCNF}). We demonstrate the applicability and scalability of $\textnormal{Alloy}^{\textnormal{Max}}$ on a benchmark of problems. To our knowledge, $\textnormal{Alloy}^{\textnormal{Max}}$ is the first approach to enable analysis with optimality in a relational modeling language, and we believe that $\textnormal{Alloy}^{\textnormal{Max}}$ has the potential to bring a wide range of new applications to Alloy.
Fri 27 AugDisplayed time zone: Athens change
11:00 - 12:00 | Architectures & Design—Model-Driven Software EngineeringResearch Papers / Demonstrations +12h Chair(s): Luciano Baresi Politecnico di Milano, Davide Di Ruscio University of L'Aquila | ||
11:00 10mPaper | AlloyMax: Bringing Maximum Satisfaction to Relational SpecificationsDistinguished Paper Award Research Papers Changjian Zhang Carnegie Mellon University, Ryan Wagner Carnegie Mellon University, Pedro Orvalho INESC-ID; Universidade de Lisboa, David Garlan Carnegie Mellon University, Vasco Manquinho INESC-ID; Universidade de Lisboa, Ruben Martins Carnegie Mellon University, Eunsuk Kang Carnegie Mellon University DOI | ||
11:10 10mPaper | Timely and Accurate Detection of Model Deviation in Self-Adaptive Software-Intensive Systems Research Papers Yanxiang Tong Nanjing University, Yi Qin Nanjing University, Yanyan Jiang Nanjing University, Chang Xu Nanjing University, Chun Cao Nanjing University, Xiaoxing Ma Nanjing University DOI | ||
11:20 5mPaper | Sangrahaka: A Tool for Annotating and Querying Knowledge Graphs Demonstrations DOI | ||
11:25 5mPaper | GenSys: A Scalable Fixed-Point Engine for Maximal Controller Synthesis over Infinite State Spaces Demonstrations Stanly Samuel Indian Institute of Science, India, Deepak D'Souza IISc Bangalore, Raghavan Komondoor IISc Bengaluru DOI Pre-print | ||
11:30 30mLive Q&A | Q&A (Architectures & Design—Model-Driven Software Engineering) Research Papers |