A Semantic Framework and Tool Support for Unified Executable Domain Models in UDML: A Case Study on the RBAC Concern

Abstract

In Domain-Driven Design (DDD), domain models play a central role in capturing domain knowledge and aligning domain experts with software developers. Although UML/OCL and
domain-specific languages (DSLs)—particularly annotation-based DSLs—enhance expressiveness
for structural and behavioral modeling, they generally lack formally defined executable semantics.
Consequently, domain models that integrate multiple concerns from different perspectives are prone
to semantic ambiguities and provide limited support for systematic correctness analysis. In contrast, formal methods offer mathematically precise semantics and proof-based verification, but remain
largely disconnected from concern-oriented and annotation-driven domain modeling practices. This
paper introduces a unified semantic framework, together with tool support, for executable domain
models. Specifically, we define a language called UDML (Unified Domain Model Language) to represent domain models in which concerns specified by corresponding DSLs are composed and share
a common system state. We focus on three key concerns—structural constraints, domain behavior,
and access policies—and define three corresponding DSLs: DCSL, AGL, and RBACDom. We then
provide a semantic framework for the unified domain model and a transformation to Event-B. This
framework enables the characterization and verification of domain model executions, while ensuring
model consistency. We validate our approach through a realistic case study based on Open Journal
Systems (OJS), demonstrating the feasibility and effectiveness of the proposed unified executable
domain modeling framework.
Keywords: Domain Driven Design, Domain Specific Language, Event-B, UDML, RBAC.