  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.
