Create Contract-based design section (in progress).
Change-Id: Idb83a64039249399bf8df6d9348a393da3c57563
diff --git a/features.html b/features.html
index 7c155be..f584ffe 100644
--- a/features.html
+++ b/features.html
@@ -3,19 +3,20 @@
<link rel="icon" type="image/png" href="favicon.ico" />
<head>
- <meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
- <title>CHESS</title>
- <link rel="stylesheet" href="styles.css" type="text/css" />
+<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
+<title>CHESS</title>
+<link rel="stylesheet" href="styles.css" type="text/css" />
</head>
<body>
- <header>
+ <header>
<div class="logo-left width">
- <a href="index.html"><img src="images/logo_chess_350.gif" alt="CHESS logo" width=""></a>
+ <a href="index.html"><img src="images/logo_chess_350.gif"
+ alt="CHESS logo" width=""></a>
</div>
- </header>
- <nav>
-
+ </header>
+ <nav>
+
<div class="width">
<ul>
<li class="start"><a href="index.html">Home</a></li>
@@ -27,212 +28,303 @@
<li><a href="events.html">Events</a></li>
<li class="divider-vertical-second-menu"></li>
<li class="end"><a href="community.html">Community</a></li>
- <li style="text-align:right;"><a href="download.html" class="box">Download</a></li>
- <li style="float:none;"><br style="clear:both;" /></li>
- </ul>
+ <li style="text-align: right;"><a href="download.html"
+ class="box">Download</a></li>
+ <li style="float: none;"><br style="clear: both;" /></li>
+ </ul>
</div>
-
- </nav>
+
+ </nav>
<div id="hrdiv">
<img src="images/bg_breadcrumb.jpg" width="" alt="" height="" />
</div>
- <div id="body" class="width-started">
+ <div id="body" class="width-started">
<article class="expanded">
<ul class="tabs">
- <li>
- <input name="tabs" id="tab1" checked="" type="radio">
+ <li><input name="tabs" id="tab1" checked="" type="radio">
<label for="tab1">Features</label>
<div id="tab-content1" class="tab-content">
<p>
<h3>CHESS Profile</h3>
- <p>
- The CHESS UML profile:
- <ul class="listInTabs">
- <li>restricts the set of MARTE, SysML and UML entities that can be created in the CHESS model, </li>
- <li>provides the set of stereotypes required to enable the user to work with the CHESS
- component model, </li>
- <li>provides some MARTE stereotypes extensions to allow the specification of
- computation-independent real-time properties, </li>
- <li>defines a new set of stereotypes for the support of dependability modeling and contract-based design.</li>
- </ul>
- </p>
- <p>
- <h3>CHESS Editor</h3>
- <p>
- The CHESS editor extends the Papyrus UML editor and is activated when a CHESS model is created
- or opened (see <a href="#figure1">Figure 1</a>).
- </p>
- <p>
- A CHESS model is a UML model with the CHESS profile applied to it; creating a CHESS model and
- applying the CHESS profile can be done using a dedicated wizard.
- </p>
- <p>
- The CHESS editor allows working with the Papyrus UML by using the CHESS design views.
- Each design view applies specific constraints on the UML diagrams and entities that can be
- created, viewed or edited in that view.
- </p>
- <p>
- The CHESS editor allows switching between views. It also keeps the status of the current view
- and during the modeling activity prevents the modeler from violating the constraints defined for
- the current diagram-view pair.
- </p>
- <p>
- The native Papyrus palettes have been customized in order to show only the entities that are
- allowed to be created in the current diagram view.
- </p>
- <p>
- <h4>CHESS Views</h4>
- <p>
- The views defined in CHESS are the requirement, system, component, deployment and analysis views.
- </p>
- <p>
- The requirement view is used to model requirements by using the standard requirement diagram
- from SysML.
- </p>
- <p>
- </p>
- <p>
- The system view is used to model system entities by using SysML; it is an ongoing development
- that has been recently introduced in CHESS in order to support the system to software
- co-engineering phase.
- </p>
- <p>
- The component view is used to model CHESS software components (also called the PIM model):
- is actually composed by two sub-views, the functional and the extra-functional ones, according
- to the CHESS separation of concerns principle.
- </p>
- <p>
- The functional view allows the functional specification of the CHESS components (see <a href="#figure1">Figure 1</a>
- and <a href="#figure2">Figure 2</a>).
- </p>
- <p>
-
- <a id="figure1"><img style="background: #fff; box-shadow: 0px 0px 6px #111;" alt="CHESS Component View Types" src="images/compFunViewTypes.png" width="85%"/></a>
- <div class="caption">Figure 1: Component View - Functional View - Component Types</div>
- </p>
- <p>
- <a id="figure2"><img style="background: #fff; box-shadow: 0px 0px 6px #111;" alt="CHESS Component View Instances" src="images/compFunViewInstances.png" width="85%"/></a>
- <div class="caption">Figure 2: Component View - Functional View - Component Instances</div>
- </p>
- <p>
- The extra functional view (see <a href="#figure3">Figure 3</a>) allows the specification of real time properties
- like periodic and sporadic activation patterns, worst-case execution time and deadline.
- Regarding dependability it supports the specification of error models (i.e. fault-error-failure
- chains) for software and offers the possibility for the user to specify probabilistic values
- related to fault occurrence and failure propagation between components.
- </p>
- <p>
- <a id="figure3"><img style="background: #fff; box-shadow: 0px 0px 6px #111;" alt="CHESS Component View Extra Functional View" src="images/compExtraFunViewInstances.jpg" width="85%"/></a>
- <div class="caption">Figure 3: Component View - Extra Functional View - Component Instances</div>
- </p>
- <p>
- The deployment view (<a href="#figure4">Figure 4</a>) is used to describe the hardware platform where the software runs
- (i.e. CPUs, buses) and software to hardware components allocation. Dependability properties can be
- provided for the hardware as for the software components. Moreover failures propagation from hardware to
- software can be specified.
- </p>
- <p>
- <a id="figure4"><img style="background: #fff; box-shadow: 0px 0px 6px #111;" alt="CHESS Deployment View" src="images/deplView.jpg" width="85%"/></a>
- <div class="caption">Figure 4: Deployment View - HW Component instance and SW allocation</div>
- </p>
- <p>
- The analysis view (<a href="#figure5">Figure 5</a>) is used to provide information needed to run the specific analysis;
- in particular it is currently useful to set the information about the dependability measure of interest
- (i.e. reliability or availability) that needs to be evaluated.
- </p>
- <p>
- <a id="figure5"><img style="background: #fff; box-shadow: 0px 0px 6px #111;" alt="CHESS Analysis View" src="images/analView.jpg" width="85%"/></a>
- <div class="caption">Figure 5: Analysis View</div>
- </p>
- <p>
- <h3>Model validator</h3>
- <p>
- For reasons of practicality, not all the constraints posed by the CHESS methodology on the model
- formalisms and contents can be enforced on the fly during user modeling; some of them must be
- checked in a batch mode. To this end the CHESS editor extends the standard UML model validator
- which ad-hoc checks that the user model conforms with the constraints imposed by the CHESS
- methodology, for example the well-formedness of entities, attributes, relations.
- </p>
- <p>
- <a id="figure6"><img style="background: #fff; box-shadow: 0px 0px 6px #111;" alt="Invoking CHESS model validator" src="images/callModelValidator.png" width="85%"/></a>
- <div class="caption">Figure 6: Invoking CHESS model validator</div>
- </p>
- <p>
- <h3>Model transformations</h3>
- <p>
- CHESS supports model-based analysis of the systems for schedulability, dependability, as
- well as code generation from model. Both features are implemented through model transformations
- which are invoked through the CHESS editor menu.
- <p>
- Dependability analysis currently supported are:
- <ul class="listInTabs">
- <li>failure propagation analysis,</li>
- <li>state-based quantitative analysis.</li>
- </ul>
- </p>
- Integration with OCRA external tool for formal verification of contract refinement is implemented.
- </p>
- <h4>Schedulability Analysis and Ada 2005 Code Generation</h4>
- <p>
- Schedulability analysis allows the calculation of the worst case response time for each declared
- periodic or sporadic activity. The analysis results are back propagated to the proper PIM
- components, also a summary report is provided to the user (see <a href="#figure7">Figure 7</a>). The intent of the
- back-propagation feature is that the user need not be concerned with the specifics of the
- analysis tool and need not learn its input and output formats: back-propagation decorates
- the user model with the relevant information that results from the analysis in full transparency
- from the analysis engine and its actual operation.
- </p>
- <p>
- <a id="figure7"><img style="background: #fff; box-shadow: 0px 0px 6px #111;" alt="CHESS Schedulability Analysis Report" src="images/schedAnalReport.png" width="85%"/></a>
- <div class="caption">Figure 7: Schedulability Analysis Report</div>
- </p>
- <p>
- The real-time properties of interest like period, offset and minimal inter-arrival time are
- specified in the model through a dedicated declarative language defined in the CHESS profile.
- The aforementioned properties are then automatically applied to the model implementation through
- model transformation in accord with the computational model chosen by the user. At the present
- time, CHESS supports the Ravenscar Computational Model [1] which meets the requirements of a
- large spectrum of real-time application domains. The generated implementation (called the PSM,
- for platform-specific model) is then given in input to the schedulability analysis and it also
- used during the code generation phase:
- </p>
- <p>
- The preservation of other real-time properties related to the execution time like WCET and
- deadline is also enforced in the generated code through dedicated checks by using specific
- API of the target run-time environment (this feature is an on-going development).
- </p>
- <p>
- This approach guarantees the preservation of the real-time properties statically assumed in the
- PIM and PSM models, and verified by the analysis down to the code.
- </p>
- <p>
- The schedulability analysis is performed by using an adaptation of the third-party MAST tool
- developed and distributed by the University of Cantabria [2].
- </p>
- <p>
- Regarding the transformation chain (<a href="#figure8">Figure 8</a>), first the CHESS PIM is transformed into the
- PSM model by using QVT-o. Then the PSM is transformed into the MAST input by using Acceleo and
- Java. Regarding the back propagation, Java is used first to load the MAST results into the PSM,
- then QVT-o traces are used to propagate the results back to the PIM model.
- </p>
- <p>
- <a id="figure8"><img style="background: #fff; box-shadow: 0px 0px 6px #111;" alt="CHESS Transformation chain" src="images/transChain.png" width="85%"/></a>
- <div class="caption">Figure 8: Transformation chain</div>
- </p>
- <p>
- [1]A. Burns, B. Dobbing, T. Vardanega. Guide to the Use of the Ada Ravenscar Profile in High Integrity Systems. Technical Report YCS-2003-348. University of York (UK), 2003. Available at <a href="http://www.sigada.org/ada_letters/jun2004/ravenscar_article.pdf"> http://www.sigada.org/ada_letters/jun2004/ravenscar_article.pdf.</a> </br>
-
-
- [2]Universidad de Cantabria. Mast: Modeling and Analysis Suite for Real-Time Applications. <a href="http://mast.unican.es/"> http://mast.unican.es/</a>
-
- </p>
- </li>
-
-
-
-
+ <p>The CHESS UML profile:
+ <ul class="listInTabs">
+ <li>restricts the set of MARTE, SysML and UML entities that
+ can be created in the CHESS model,</li>
+ <li>provides the set of stereotypes required to enable the
+ user to work with the CHESS component model,</li>
+ <li>provides some MARTE stereotypes extensions to allow the
+ specification of computation-independent real-time properties,</li>
+ <li>defines a new set of stereotypes for the support of
+ dependability modeling and contract-based design.</li>
+ </ul>
+ </p>
+ <p>
+ <h3>CHESS Editor</h3>
+ <p>
+ The CHESS editor extends the Papyrus UML editor and is activated
+ when a CHESS model is created or opened (see <a href="#figure1">Figure
+ 1</a>).
+ </p>
+ <p>A CHESS model is a UML model with the CHESS profile applied
+ to it; creating a CHESS model and applying the CHESS profile can
+ be done using a dedicated wizard.</p>
+ <p>The CHESS editor allows working with the Papyrus UML by
+ using the CHESS design views. Each design view applies specific
+ constraints on the UML diagrams and entities that can be created,
+ viewed or edited in that view.</p>
+ <p>The CHESS editor allows switching between views. It also
+ keeps the status of the current view and during the modeling
+ activity prevents the modeler from violating the constraints
+ defined for the current diagram-view pair.</p>
+ <p>The native Papyrus palettes have been customized in order
+ to show only the entities that are allowed to be created in the
+ current diagram view.</p>
+ <p>
+ <h4>CHESS Views</h4>
+ <p>The views defined in CHESS are the requirement, system,
+ component, deployment and analysis views.</p>
+ <p>The requirement view is used to model requirements by using
+ the standard requirement diagram from SysML.</p>
+ <p></p>
+ <p>The system view is used to model system entities by using
+ SysML; it is an ongoing development that has been recently
+ introduced in CHESS in order to support the system to software
+ co-engineering phase.</p>
+ <p>The component view is used to model CHESS software
+ components (also called the PIM model): is actually composed by
+ two sub-views, the functional and the extra-functional ones,
+ according to the CHESS separation of concerns principle.</p>
+ <p>
+ The functional view allows the functional specification of the
+ CHESS components (see <a href="#figure1">Figure 1</a> and <a
+ href="#figure2">Figure 2</a>).
+ </p>
+ <p>
+
+ <a id="figure1"><img
+ style="background: #fff; box-shadow: 0px 0px 6px #111;"
+ alt="CHESS Component View Types"
+ src="images/compFunViewTypes.png" width="85%" /></a>
+ <div class="caption">Figure 1: Component View - Functional
+ View - Component Types</div>
+ </p>
+ <p>
+ <a id="figure2"><img
+ style="background: #fff; box-shadow: 0px 0px 6px #111;"
+ alt="CHESS Component View Instances"
+ src="images/compFunViewInstances.png" width="85%" /></a>
+ <div class="caption">Figure 2: Component View - Functional
+ View - Component Instances</div>
+ </p>
+ <p>
+ The extra functional view (see <a href="#figure3">Figure 3</a>)
+ allows the specification of real time properties like periodic
+ and sporadic activation patterns, worst-case execution time and
+ deadline. Regarding dependability it supports the specification
+ of error models (i.e. fault-error-failure chains) for software
+ and offers the possibility for the user to specify probabilistic
+ values related to fault occurrence and failure propagation
+ between components.
+ </p>
+ <p>
+ <a id="figure3"><img
+ style="background: #fff; box-shadow: 0px 0px 6px #111;"
+ alt="CHESS Component View Extra Functional View"
+ src="images/compExtraFunViewInstances.jpg" width="85%" /></a>
+ <div class="caption">Figure 3: Component View - Extra
+ Functional View - Component Instances</div>
+ </p>
+ <p>
+ The deployment view (<a href="#figure4">Figure 4</a>) is used to
+ describe the hardware platform where the software runs (i.e.
+ CPUs, buses) and software to hardware components allocation.
+ Dependability properties can be provided for the hardware as for
+ the software components. Moreover failures propagation from
+ hardware to software can be specified.
+ </p>
+ <p>
+ <a id="figure4"><img
+ style="background: #fff; box-shadow: 0px 0px 6px #111;"
+ alt="CHESS Deployment View" src="images/deplView.jpg"
+ width="85%" /></a>
+ <div class="caption">Figure 4: Deployment View - HW
+ Component instance and SW allocation</div>
+ </p>
+ <p>
+ The analysis view (<a href="#figure5">Figure 5</a>) is used to
+ provide information needed to run the specific analysis; in
+ particular it is currently useful to set the information about
+ the dependability measure of interest (i.e. reliability or
+ availability) that needs to be evaluated.
+ </p>
+ <p>
+ <a id="figure5"><img
+ style="background: #fff; box-shadow: 0px 0px 6px #111;"
+ alt="CHESS Analysis View" src="images/analView.jpg" width="85%" /></a>
+ <div class="caption">Figure 5: Analysis View</div>
+ </p>
+ <p>
+ <h3>Model validator</h3>
+ <p>For reasons of practicality, not all the constraints posed
+ by the CHESS methodology on the model formalisms and contents can
+ be enforced on the fly during user modeling; some of them must be
+ checked in a batch mode. To this end the CHESS editor extends the
+ standard UML model validator which ad-hoc checks that the user
+ model conforms with the constraints imposed by the CHESS
+ methodology, for example the well-formedness of entities,
+ attributes, relations.</p>
+ <p>
+ <a id="figure6"><img
+ style="background: #fff; box-shadow: 0px 0px 6px #111;"
+ alt="Invoking CHESS model validator"
+ src="images/callModelValidator.png" width="85%" /></a>
+ <div class="caption">Figure 6: Invoking CHESS model
+ validator</div>
+ </p>
+ <p>
+ <h3>Model transformations</h3>
+ <p>CHESS supports model-based analysis of the systems for
+ schedulability, dependability, as well as code generation from
+ model. Both features are implemented through model
+ transformations which are invoked through the CHESS editor menu.
+
+
+
+ <p>Dependability analysis currently supported are:
+ <ul class="listInTabs">
+ <li>failure propagation analysis,</li>
+ <li>state-based quantitative analysis.</li>
+ </ul>
+ </p>
+ Integration with OCRA external tool for formal verification of
+ contract refinement is implemented.
+ </p>
+ <h4>Schedulability Analysis and Ada 2005 Code Generation</h4>
+ <p>
+ Schedulability analysis allows the calculation of the worst case
+ response time for each declared periodic or sporadic activity.
+ The analysis results are back propagated to the proper PIM
+ components, also a summary report is provided to the user (see <a
+ href="#figure7">Figure 7</a>). The intent of the
+ back-propagation feature is that the user need not be concerned
+ with the specifics of the analysis tool and need not learn its
+ input and output formats: back-propagation decorates the user
+ model with the relevant information that results from the
+ analysis in full transparency from the analysis engine and its
+ actual operation.
+ </p>
+ <p>
+ <a id="figure7"><img
+ style="background: #fff; box-shadow: 0px 0px 6px #111;"
+ alt="CHESS Schedulability Analysis Report"
+ src="images/schedAnalReport.png" width="85%" /></a>
+ <div class="caption">Figure 7: Schedulability Analysis
+ Report</div>
+ </p>
+ <p>The real-time properties of interest like period, offset
+ and minimal inter-arrival time are specified in the model through
+ a dedicated declarative language defined in the CHESS profile.
+ The aforementioned properties are then automatically applied to
+ the model implementation through model transformation in accord
+ with the computational model chosen by the user. At the present
+ time, CHESS supports the Ravenscar Computational Model [1] which
+ meets the requirements of a large spectrum of real-time
+ application domains. The generated implementation (called the
+ PSM, for platform-specific model) is then given in input to the
+ schedulability analysis and it also used during the code
+ generation phase:</p>
+ <p>The preservation of other real-time properties related to
+ the execution time like WCET and deadline is also enforced in the
+ generated code through dedicated checks by using specific API of
+ the target run-time environment (this feature is an on-going
+ development).</p>
+ <p>This approach guarantees the preservation of the real-time
+ properties statically assumed in the PIM and PSM models, and
+ verified by the analysis down to the code.</p>
+ <p>The schedulability analysis is performed by using an
+ adaptation of the third-party MAST tool developed and distributed
+ by the University of Cantabria [2].</p>
+ <p>
+ Regarding the transformation chain (<a href="#figure8">Figure
+ 8</a>), first the CHESS PIM is transformed into the PSM model by
+ using QVT-o. Then the PSM is transformed into the MAST input by
+ using Acceleo and Java. Regarding the back propagation, Java is
+ used first to load the MAST results into the PSM, then QVT-o
+ traces are used to propagate the results back to the PIM model.
+ </p>
+ <p>
+ <a id="figure8"><img
+ style="background: #fff; box-shadow: 0px 0px 6px #111;"
+ alt="CHESS Transformation chain" src="images/transChain.png"
+ width="85%" /></a>
+ <div class="caption">Figure 8: Transformation chain</div>
+ </p>
+ <p>
+ [1]A. Burns, B. Dobbing, T. Vardanega. Guide to the Use of the
+ Ada Ravenscar Profile in High Integrity Systems. Technical Report
+ YCS-2003-348. University of York (UK), 2003. Available at <a
+ href="http://www.sigada.org/ada_letters/jun2004/ravenscar_article.pdf">
+ http://www.sigada.org/ada_letters/jun2004/ravenscar_article.pdf.</a>
+ </br> [2]Universidad de Cantabria. Mast: Modeling and Analysis Suite
+ for Real-Time Applications. <a href="http://mast.unican.es/">
+ http://mast.unican.es/</a>
+
+ </p></li>
+
+ <li><input name="tabs" id="tab2" type="radio"> <label
+ for="tab2">Contract-based design</label>
+ <div id="tab-content2" class="tab-content">
+ <p>The contract-based design enriches the system architecture
+ model with expressions asserting the expected properties of the
+ system, its components and environment. In order to allow
+ compositional reasoning, the property of a component are
+ restricted to its interface considering the component as a black
+ box (without constraining the internal variables of the
+ component) and are structured into contracts, pairs of properties
+ representing an assumption and a guarantee of the component: an
+ assumption is an assertion on the behaviour of the component
+ environment, while a guarantee is an assertion on the behaviour
+ of the component provided that the entire set of assumptions
+ holds.</p>
+ <p>CHESS supports the specification of contracts with the help
+ of an automated completion feature that suggests the possible
+ continuations of a partial specification.<p>
+ <a id="figure1"><img
+ style="background: #fff; box-shadow: 0px 0px 6px #111;"
+ alt="Property Editor with “completion assistance”"
+ src="images/contract-editor.png" width="85%" /></a>
+
+ <div class="caption">Property Editor with “completion
+ assistance”</div>
+ </p>
+ <p>If assumptions and guarantees are formal properties, which
+ means they are specified in a formal language such as some
+ specific kind of temporal logic, the architectural decomposition
+ can be verified by checking that the contract refinement is
+ correct: this consists of checking that, for all composite
+ components, the contract of the composite component is ensured by
+ the contracts of the subcomponents –considering their
+ interconnection as described by the architecture -and that the
+ assumption of each subcomponent is ensured by the contracts of
+ the other sibling subcomponents and the assumption of the
+ composite component.</p>
+ <p>
+ <a id="figure2"><img
+ style="background: #fff; box-shadow: 0px 0px 6px #111;"
+ alt="An example of the result of the check
+ contract refinement shown in the Trace View."
+ src="images/contract-refinement.png" width="85%" /></a>
+
+ <div class="caption">An example of the result of the check
+ contract refinement shown in the Trace View. In this case, it is
+ possible to see that one refinement is failed, and the counter
+ example.</div>
+ </p>
+ </div></li>
+
+
<!--li>
<input name="tabs" id="tab2" type="radio">
<label for="tab2">Example</label>
@@ -255,20 +347,23 @@
</p>
</div>
</li-->
-
+
</ul>
- </article>
- </div>
-
+ </article>
+ </div>
+
<div class="clear"></div>
-
- <footer id="footer-features">
+
+ <footer id="footer-features">
<div class="footer-content width">
<ul>
<li><h4>Eclipse Foundation</h4></li>
<li><a href="https://www.eclipse.org/org/">About</a></li>
- <li><a href="https://www.eclipse.org/org/foundation/contact.php">Contact Us</a></li>
- <li><a href="https://projects.eclipse.org/projects/polarsys.chess">CHESS
+ <li><a
+ href="https://www.eclipse.org/org/foundation/contact.php">Contact
+ Us</a></li>
+ <li><a
+ href="https://projects.eclipse.org/projects/polarsys.chess">CHESS
Project Page</a></li>
</ul>
<ul>
@@ -292,12 +387,13 @@
<li><a
href="https://wiki.eclipse.org/CHESS/Technical_Information">How
to Contribute</a></li>
- <li><a href="https://accounts.eclipse.org/mailing-list/chess-dev">Mailing
+ <li><a
+ href="https://accounts.eclipse.org/mailing-list/chess-dev">Mailing
List</a></li>
<li><a href="https://www.eclipse.org/forums/index.php/f/529/">Forum</a></li>
</ul>
<ul class="endfooter">
- <li><h4>Other</h4></li>
+ <li><h4>Other</h4></li>
<li><a href="https://es.fbk.eu/">Fondazione Bruno Kessler</a></li>
<li><a href="http://www.intecs.it/">Intecs</a></li>
<li><a href="http://www.unipd.it">University of Padova</a></li>
@@ -320,7 +416,7 @@
All Rights Reserved.
</div>
</td>
- </tr>
+ </tr>
</table>
<div class="clear"></div>
diff --git a/images/contract-editor.png b/images/contract-editor.png
new file mode 100644
index 0000000..957d0af
--- /dev/null
+++ b/images/contract-editor.png
Binary files differ
diff --git a/images/contract-refinement.png b/images/contract-refinement.png
new file mode 100644
index 0000000..0fc093a
--- /dev/null
+++ b/images/contract-refinement.png
Binary files differ
