Refinement and verification in component-based model-driven design

Zhenbang Chen, Zhiming Liu, Anders Peter Ravn, Volker Stolz, Naijun Zhan

Research output: Contribution to journalJournal articleResearchpeer-review

38 Citations (Scopus)


Modern software development is complex as it has to deal with many different and yet related aspects of applications. In practical software engineering this is now handled by a UML-like modelling approach in which different aspects are modelled by different notations. Component-based and object-oriented design techniques are found effective in the support of separation of correctness concerns of different aspects. These techniques are practiced in a model-driven development process in which models are constructed in each phase of the development. To ensure the correctness of the software system developed, all models constructed in each phase are verifiable. This requires that the modelling notations are formally defined and related in order to have tool support developed for the integration of sophisticated checkers, generators and transformations. This paper summarises our research on the method of Refinement of Component and Object Systems (rCOS) and illustrates it with experiences from the work on the Common Component Modelling Example (CoCoME). This gives evidence that the formal techniques developed in rCOS can be integrated into a model-driven development process and shows where it may be integrated in computer-aided software engineering (CASE) tools for adding formally supported checking, transformation and generation facilities.
Original languageEnglish
JournalScience of Computer Programming
Issue number4
Pages (from-to)168-196
Number of pages29
Publication statusPublished - 2009



  • Formal methods; Multi-view modelling; rCOS; Software design process; Tool design; UML

Cite this