The rCOS Modeler: model-driven development and integrated verification support

Title: The rCOS Modeler: model-driven development and integrated verification support
Speaker: Dr. Volker Stolz （International Institute for Software Technology,United Nations University, Macao）
Time: 3：00pm, Monday，March.9
Venue: Lecture Room,State Key Lab of Computer Science, Level 3 Building #5, Institute of Software, CAS

Abstract: The rCOS Modeling Tool implements the rCOS methodology: it supports use-case driven requirements capture in a multi-view notation. UML class-, sequence, and state diagrams (restricted by the rCOS UML profile) capture the structure and dynamic behaviour of a use case. This separates the different concerns of this stage from each other. Methods of classes are specified with UTP-style pre/post conditions. Static (typing) and dynamic (behaviour in terms of process algebra CSP) consistency of these views are enforced. rCOS contracts specify the component interface (with behaviour usually described in the dynamic diagrams). Component composition can then be verified again through a process algebra, so this task is also delegated to CSP and FDR2.

After the Requirements Modeling stage, the rCOS tool supports various transformations for refinement and verification:
– OO refinement (Expert Pattern) – Integration (reactive system based on state machine and functionality specification)
– Abstraction (elimination of attributes/data)

The bio of the speaker:
Dr. Volker Stolz is an Assistant Research Fellow at the United Nations University International Institute for Software Technology (UNU-IIST). He is a member in the `rCOS’ research group working in the “Harnessing Theories for Tool support in Software” project funded by the Macao Science and Technology Development Fund, working on applying formal methods and verification techniques to component based software engineering.

He holds a diploma in Computer Science and a PhD degree from RWTH Aachen University, Germany. He is in the program committee of various workshops and lecturer in UNU-IIST courses.His interests include applied formal methods, programming language design, and logic programming.