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.
翻译:软件产品的质量往往与设计过程早期所采用抽象的质量相关。认识到这一趋势后,人们开发了各种工具和方法论,旨在实现系统前对其进行全面建模。然而,创建有效的领域问题抽象模型是困难的,尤其当这些模型还需具备诸如直观性、可与其他模型无缝集成或易于转化为代码等特性时。本论文描述了Conceptual,这是一种用于通过称为概念的自包含、高可复用功能单元来建模软件系统行为的领域特定语言。该语言的语法和语义基于先前工作进行了形式化定义。此外,论文提出了一种将Conceptual语言结构映射至Alloy建模语言的策略。该策略通过一个简易编译器实现,使开发者能够访问并利用Alloy现有的程序推理分析工具。通过多个实际案例研究,定性地论证了Conceptual的实用性与表达力。借助所实现的编译器,在现有文献中识别出若干错误规约。此外,本论文还在Visual Studio Code集成开发环境中建立了初步的工具支持。