Commit 61c291df authored by Bernhard Rumpe's avatar Bernhard Rumpe
Browse files

BR

parent e726276a
<h2>Modal Object Diagrams</h2>
S. Maoz, J.O. Ringert, and B. Rumpe
<p>
While object diagrams (ODs) are widely used as a means to document object-oriented systems, they are expressively weak, as they are limited to describe specific possible snapshots of the system at hand. In this paper we introduce <strong>modal object diagrams</strong> (MODs), which extend the classical OD language with positive/negative and example/invariant modalities. The extended language allows the designer to specify not only positive example models but also negative examples, ones that the system should not allow, positive invariants, ones that all system's snapshots should include, and negative invariants, ones that no system snapshot is allowed to include. Moreover, as a primary application of the extended language we provide a formal verification technique that decides whether a given class diagram satisfies (i.e., models) a multi-modal object diagrams specification. In case of a negative answer, the technique outputs relevant counterexample object models, as applicable. The verification is based on a reduction to Alloy. The ideas are implemented in a prototype Eclipse plug-in. Examples show the usefulness of the extended language in specifying structural requirements of object-oriented systems in an intuitive yet expressive way.
</p>
<h3>Publications</h3>
S. Maoz, J.O. Ringert, and B. Rumpe. <strong>Modal Object Diagrams</strong>. In ECOOP 2011.
[<a href="http://www.se-rwth.de/~maoz/papers/mod-ecoop11.pdf">pdf</a>]
<br>
<br>
<p>
<h3>Supporting materials</h3>
<ul><li> <a href="mod-plugin.zip">MOD plug-in</a> prototype implementation (download as plug-in for Eclipse 3.6)
</li>
<li> <a href="MODPluginReadme.pdf">MOD plug-in readme and installation instructions</a>
</li>
<li> <a href="mod-examples.zip">Example CDs and MODs</a>
</li>
</ul>
</p>
\ No newline at end of file
<?php
$ROOT_PATH = "../../";
$TITLE = "SE@RWTH : Modal Object Diagrams";
include ($ROOT_PATH."layout/lib.php");
include ($ROOT_PATH."layout/header.php");
include ("content.php");
include ($ROOT_PATH."layout/footer.php");
?>
\ No newline at end of file
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment