Establishing tool support for a concept DSL

TL;DR

The work addresses the challenge of creating high-quality abstractions early in software design by formalizing Conceptual, a DSL that models software behavior as reusable concepts. It develops a strategy to translate Conceptual into Alloy, and implements a practical OCaml-based compiler that outputs Alloy modules for analysis with Alloy’s model finder. Through case studies, the approach demonstrates expressiveness and reveals design flaws in existing literature, while establishing initial tool support in Visual Studio Code. This combination of formal language design, translation to a decidable analysis target, and preliminary tooling advances concept-based modeling as a viable pathway for rigorous, modular system design and verification.

Abstract

The quality of software products tends to correlate with the quality of the abstractions adopted early in the design process. Acknowledging this tendency has led to the development of various tools and methodologies for modeling systems thoroughly before implementing them. However, creating effective abstract models of domain problems is difficult, especially if the models are also expected to exhibit qualities such as intuitiveness, being seamlessly integrable with other models, or being easily translatable into code. This thesis describes Conceptual, a DSL for modeling the behavior of software systems using self-contained and highly reusable units of functionally known as concepts. The language's syntax and semantics are formalized based on previous work. Additionally, the thesis proposes a strategy for mapping language constructs from Conceptual into the Alloy modeling language. The suggested strategy is then implemented with a simple compiler, allowing developers to access and utilize Alloy's existing analysis tools for program reasoning. The utility and expressiveness of Conceptual is demonstrated qualitatively through several practical case studies. Using the implemented compiler, a few erroneous specifications are identified in the literature. Moreover, the thesis establishes preliminary tool support in the Visual Studio Code IDE.

Figures (17)

• Figure 1: Graphical representation of the thesis structure. Solid lines depict dependencies between chapters, whereas the dotted lines associate appendices with specific chapters.
• Figure 2: Overall compiler architecture and phases.
• Figure 3: Graphical representation of the compiler design methodology from section \ref{['sec:compiler_method']}.
• Figure 4: Example of a unit test where a node in the was changed from a conjunction to a disjunction to simulate a fault in the parser. The test catches the misbehavior and highlights the discrepancies from the expected parse tree.
• Figure 5: Example to explain frame conditions. The left snippet is part of the reservation concept in JacksonConcepts. The right snippet is a translation to Alloy. The operator refers to the value of a mutable expression in the subsequent state. It may be nested.