rCOS

Refinement of Component and Object Systems

  • Increase font size
  • Default font size
  • Decrease font size

rCOS Modeler Release Notes v1.2.2

E-mail Print PDF

New features in the rCOS Requirements Modeler v.1.2.2 (June 30th 2009):

  • Syntax checking in the graphical modeler (guards, invariants, and designs). However, since we don't have a full type-checker yet, you will get spurious type checking errors. Just ignore them, your input is still accepted.

  • Integration, Expert Pattern and Abstraction transformations (cf. FSEN'09). In the CoCoME-exe example, go to the "Transformations"-package and open the class diagram. You can either run the Integrate and Abstract transformations separately, or choose IntegrateAndAbstract to run both transformations chained together. Simply right-click on a class and choose the operation from the rCOS sub-menu (see screenshot). The parameters of the transformations can be set in the "Properties" tab. You can also run the expert pattern directly on a class or operation through the context menu. Any errors will be logged in the Error view. Note that any changes to classes in the diagrams are not visible unless you manually select "Refresh Class" from the menu (to be automated).

  • CSP export. A (suitably abstracted, see above) class can be translated into CSP. The above example also contains an item for this. Note that manual editing of the generated CSP is still required if there are e.g. parameters on events.

  • Library/Imports framework (handles e.g. sets and some input/output helpers).

  • Model validation: use the green checkmark in the modeler to validate your model. Error markers will show up on the affected elements, and a problem description will be given in the Problems View.

  • UTF-8 encoding support for mathematical characters:
    [ true ⊢∀LineItem l∊∀Item p∊(sale.lines.contains(l) ... ]
  • Undo/Redo support in editor, also for the model transformations.

  • Automated refinement. Most of the simple specifications like pre/post with dashed variables can automatically be refined to executable designs. See the CoCoME example file for an example.

  • Method calls in guards, invariants and preconditions must be side-effect free (pure). The modeler currently uses the UML query attribute on operations. A static analysis is forthcoming.

Please also see the documents about the modeler. Please send any bug reports and suggestions!

Volker & Charles

Screenshot of transformations in rCOS modeler
 

rCOS - Refinement of Component and Object Systems

E-mail Print PDF

rCOS is a notation that supports refinement and verification in component-based and object-oriented design.

The distinctive features of rCOS are:

  • it has evolved from a semantic foundation including a well-defined refinement calculus
  • it develops the Unifying Theories of Programming (UTP) to the domain of component-based designs by defining concepts like classes, objects, components, interfaces, contracts, and coordination. Further it provides the behavioural semantics of these concepts and their compositions with high level rules for refinement and verification.

The rCOS Modeler

We are developing an integrated UML modeler (ver. 1.2, Feb. 18 2009) for component-based model driven software development for Eclipse.

The rCOS group is supported by the projects HighQSoftD  and HTTS, funded by the Macau Science and Technology Fund.