Typing Requirement Model as Coroutines

TL;DR

The paper tackles ensuring correctness of REModel-based requirement models in Model-Driven Engineering by introducing a coroutine-based type system that encodes preconditions as receiving parts and postconditions as yielding parts of coroutines. It formalizes coroutine types $[t_1; t_2]$, supporting a composition operator $\circ : S \to R$ to derive a single executable view of multiple contracts, and provides detailed rules for yielding and resuming to model execution order. The approach is implemented in .NET Core 3.1 and validated on four RM2PT case studies, showing that the inferred coroutine types align with the embedded sequence diagrams and can guide integration testing; the composer also demonstrates cross-language modeling via constrained types. Limitations include handling branching and fine-grained data checks, with future work aimed at conditional expressions, contract grouping, and broader applicability beyond RM2PT.

Abstract

Model-Driven Engineering (MDE) is a technique that aims to boost productivity in software development and ensure the safety of critical systems. Central to MDE is the refinement of high-level requirement models into executable code. Given that requirement models form the foundation of the entire development process, ensuring their correctness is crucial. RM2PT is a widely used MDE platform that employs the REModel language for requirement modeling. REModel contains contract sections and other sections including a UML sequence diagram. This paper contributes a coroutine-based type system that represents pre- and post-conditions in the contract sections in a requirement model as the receiving and yielding parts of coroutines, respectively. The type system is capable of composing coroutine types, so that users can view functions as a whole system and check their collective behavior. By doing so, our type system ensures that the contracts defined in it are executed as outlined in the accompanied sequence diagram. We assessed our approach using four case studies provided by RM2PT, validating the accuracy of the models.

Figures (9)

• Figure 1: In RM2PT, Java source code can be generated from a .remodel file through its context menu
• Figure 2: The architecture of the requirement model checking framework depicted in the UML component diagram
• Figure 3: Abstract syntax for types in our coroutine type system
• Figure 4: Definition of head ${\mathbf{h}}$ and tail ${\mathbf{t}}$ of a type
• Figure 5: Definition of $\mathbf{match}$ for matching two types.