Lecturer: Zhiming Liu
Course Description:
Model driven development is a most promising approach to separation of concerns in design of complex software systems. It employs a UML-like multi-view and multi-notational language for describing the models of the system at different stages in the development. It also support component-based design and allows developers to design systems at a higher level of abstraction using models or specifications of components which will be produced and integrated at a later implementation, assembly and deployment stage.
However, a major challenge in the practice of model-based software development is to ensure correctness and dependability of the software product. To deal with this challenge, we need a common semantics for the multi-view modeling approach, and a method for verification and reasoning a out models of different views, correct refinement of models, and consistently relating the models of different views. Tool support to such a method needs to integrate sophisticated drawing and editing tools for model construction, transformers for correctness preserving model transformations, checkers and provers for verification of properties of models. The method, techniques and tools have to be incorporated (or be able to be incorporated) into existing software development processes and environment.
In this course, we introduce a method, called rCOS, that we recently developed for Refinement and Verification in Component-Based Model Driven Development. The outline of the content of the course is:
-- Introduction: the state of the art in practical software engineering, the current status of formal methods, the motivation and theme of rCOS
-- Unifying Theories of Programming (UTP) in Nutshell: the semantics foundation of rCOS
-- The formal theory of rCOS a). component-based modelling and refinement: interfaces, contracts, components, composition (connectors), coordination and glue. b). object-oriented modelling and refinement: classes, objects, references, polymorphism, subtyping, dynamic binding, oo refinement
-- Development process and case study
-- Tool support: UML profile for rCOS, model transformations and model verification and analysis
Exam: select one of:
Group project: each group of two or three can work on their own identified project by using the rCOS method. It can be an object-oriented system, a component-based project, a project that needs both component-based and object-oriented modelling and design.
Seminar: Relate rCOS to your own research interest
Course materials:
1) Slides will be given before or at the lectures 2) Downloadable publications about rCOS at http://rcos.iist.unu.edu