Typing Requirement Model as Coroutines

TL;DR

This paper introduces a coroutine-based type system for requirement models in Model-Driven Engineering, enabling better verification of contract correctness and system behavior through composition and analysis of coroutines.

Contribution

It presents a novel coroutine-based type system for requirement models that improves contract verification and system composition in MDE platforms.

Findings

The type system accurately models pre- and post-conditions as coroutines.

It enables composition of coroutine types for holistic system analysis.

Validation with four case studies confirms effectiveness.

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.