부산대학교 도서관

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.