Model-driven
development is a
most promising
approach to
separation of
concerns in
design of
complex software
systems. It
employs a UML-like
multiview and
multi-notational
language for
describing the
models of the
system at
different stages
in the
development. It
also supports
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 multiview
modeling
approach, and a
method for
verification and
reasoning about
models of
different views,
correct
refinement of
models, and
consistently
relating the
models of
different views.
Tool support for
such a method
needs to
integrate
sophisticated
drawing and
editing tools
for model
construction,
transformers for
correctness
preserving model
transformations,
and 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
environments.
The rCOS method
includes a
formal notation
and a calculus
of refinement
for specifying,
verifying and
transforming
(refining)
models of
component-based
and
object-oriented
designs at
different levels
of abstraction.
It has a UML
profile for tool
support of
building and
transforming
models and
allows the
application of
verification
tools for
analysing
models.
Outline of
topics:
-
Introduction:
the state of
the art in
practical
software
engineering,
the current
status of
formal
methods,
motivation
and theme of
rCOS.
- Semantic
root in
Unified
Theories of
Programming
(UTP, as
studied in
the
Foundations
Course).
- Theory of
rCOS:
component-based
modelling
and
refinement —
interfaces,
contracts,
components,
composition
(connectors),
coordination
and glue.
Object-oriented
modeling and
refinement –
classes,
objects,
references,
polymorphism,
subtyping,
dynamic
binding, OO
refinement.
-
Development
process and
case study.
- Tool:
UML profile
for rCOS,
model
transformations
and model
verification
and
analysis.
