diff --git a/features.html b/features.html
index 03ee564..fc805be 100644
--- a/features.html
+++ b/features.html
@@ -179,6 +179,11 @@
 							environment, while a guarantee is an assertion on the behaviour
 							of the component provided that the entire set of assumptions
 							holds.</p>
+						<p>The contract specification can further be enriched by
+							categorising contracts into strong and weak to allow for better
+							support for specification of reusable components behaviour. Such
+							components are intended to work in different environments, and
+							often exhibit environment-specific behaviours and assumptions.</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
@@ -203,7 +208,9 @@
 							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>
@@ -416,6 +423,13 @@
 							components properties. The effect must be expressed by using the
 							SMV language, to model component properties assignment.</p>
 
+						<a id="figure1"><img
+							style="background: #fff; box-shadow: 0px 0px 6px #111;"
+							alt="Example of nominal state machine" src="images/chess-FSM.png"
+							width="85%" /></a>
+						<div class="caption">Example of nominal state machine (using
+							SMV as action language)</div>
+
 						<p>The behavioural model of the component can be enriched with
 							the faulty behaviour. Faulty behaviour is modelled in CHESS by
 							using the dedicated dependability profile. The CHESS
@@ -451,6 +465,24 @@
 							possible to see that one refinement is failed, and the counter
 							example.</div>
 
+						<h4>Contract-based Verification of Refinement for Strong and
+							Weak Contracts</h4>
+
+						<p>Strong and weak contracts are introduced to support
+							out-of-context reasoning and component reuse across variety of
+							environments. While strong contracts must hold in all
+							environments, the weak ones are environment-specific. Prior to
+							performing the refinement check using strong and weak contracts,
+							contracts must be created and allocated to the component types,
+							which represent out-of-context components. At the component type
+							level, the user indicates if a contract is strong or weak. When
+							the component type is instantiated in a particular system to a
+							component instance, all the strong, and a subset of weak
+							contracts can be identified as relevant in the particular system
+							in which the component is instantiated. Identifying which are
+							those relevant weak contracts can be done manually on the
+							component instance level.</p>
+
 						<h4>Contract-Based Verification of State Machines</h4>
 
 
@@ -484,15 +516,17 @@
 							counterexample, i.e. a trace of the FSM that falsifies the
 							property.</p>
 						<p>There are three possible model checking available:</p>
-
-						- check ctlspec: it performs fair CTL model checking. A CTL
-						specification is given as a formula in the temporal logic CTL. A
-						CTL formula is true if it is true in all initial states. <br>
-						- check invar: it performs model checking of invariants.
-						Invariants are propositional formulas which must hold invariantly
-						in the model.<br> - check ltlspec: it performs LTL model
-						checking. An LTL formula is true if it is true at the initial
-						time. <br> <br>
+						<ul class="listInTabs">
+							<li>check ctlspec: it performs fair CTL model checking. A
+								CTL specification is given as a formula in the temporal logic
+								CTL. A CTL formula is true if it is true in all initial states.
+							</li>
+							<li>check invar: it performs model checking of invariants.
+								Invariants are propositional formulas which must hold
+								invariantly in the model.</li>
+							<li>check ltlspec: it performs LTL model checking. An LTL
+								formula is true if it is true at the initial time.</li>
+						</ul>
 						<h2>Safety Analysis</h2>
 						<h3>Model-Based Safety Analysis</h3>
 						<h4>Fault injection</h4>
@@ -505,13 +539,22 @@
 							state, the effect upon a property of the component, and so the
 							effect on its nominal behaviour, can be also provided by using
 							pre-defined effects:</p>
-						<br> - StuckAt: models the effect of being stuck at a fixed
-						value.<br> - StuckAtFixed: models the effect of being stuck
-						at a fixed random value.<br> - Inverted: models the effect of
-						being stuck at the inverted last value.<br> - RampDown:
-						models the effect of decreasing the value of a property by a
-						certain value.<br>
-
+						<ul class="listInTabs">
+							<li>StuckAt: models the effect of being stuck at a fixed
+								value.
+							<li>StuckAtFixed: models the effect of being stuck at a
+								fixed random value.</li>
+							<li>Inverted: models the effect of being stuck at the
+								inverted last value.</li>
+							<li>RampDown: models the effect of decreasing the value of a
+								property by a certain value.</li>
+						</ul>
+						<a id="figure1"><img
+							style="background: #fff; box-shadow: 0px 0px 6px #111;"
+							alt="State machine modelling faulty behaviour"
+							src="images/chess-fault-injection.png" width="85%" /></a>
+						<div class="caption">State machine modelling faulty
+							behaviour</div>
 						<h4>Fault-tree generation and FMEA generation</h4>
 						<p>Once the system architecture has been provided, by mean of
 							components definition and their nominal and error models, the
@@ -526,6 +569,13 @@
 							The fault tree can be examined, in particular the minimal cut-set
 							and so the basic fault conditions which can led to the top-level
 							failure.</p>
+						<a id="figure1"><img
+							style="background: #fff; box-shadow: 0px 0px 6px #111;"
+							alt="A fault tree visualized in the CHESS Editor View"
+							src="images/chess-FTA.png" width="85%" /></a>
+						<div class="caption">A fault tree visualized in the CHESS
+							Editor View; note the probabilities associated to the top and
+							basic events</div>
 						<p>Along with the fault-tree generation, it is possible to
 							generate the FMEA table. FMEA analysis is configured in a similar
 							mode as the fault-tree analysis, see the CHESS User Manual for
@@ -544,6 +594,20 @@
 							components and the failure of the system environment.</p>
 
 						<h2>Safety Case</h2>
+						<p>In most industries, a well-structured Safety-Case, i.e. a
+							concluding argument that the system to be released for public
+							usage is sufficiently safe, is required by safety standards and
+							certification authorities. Standards mentioning the obligation
+							for a Safety Case include IEC 61508, ISO 26262 and many more. The
+							notion of a Safety Case is not formally defined by the standards
+							and therefore varies among different standards, regions and
+							industry branches – it can even depend on the company who creates
+							it or on the safety assessor or local certification authority.
+							Where this term is in use, it refers at least to a collection of
+							all relevant output documents from the safety process, from which
+							an external assessor can conclude that everything has been done
+							to assure that the product is safe in its practical application.</p>
+
 						<h3>Document Generation</h3>
 						<p>As part of the evidences to be used at support of the
 							safety case, the tool can generate a document summarizing the
diff --git a/images/chess-FSM.png b/images/chess-FSM.png
new file mode 100644
index 0000000..8953b8c
--- /dev/null
+++ b/images/chess-FSM.png
Binary files differ
diff --git a/images/chess-FTA.png b/images/chess-FTA.png
new file mode 100644
index 0000000..9b3ceb1
--- /dev/null
+++ b/images/chess-FTA.png
Binary files differ
diff --git a/images/chess-fault-injection.png b/images/chess-fault-injection.png
new file mode 100644
index 0000000..ad3421d
--- /dev/null
+++ b/images/chess-fault-injection.png
Binary files differ
diff --git a/styles.css b/styles.css
index abd152f..ff6a1de 100644
--- a/styles.css
+++ b/styles.css
@@ -592,7 +592,7 @@
 }
 
 #footer-features {
-	margin: 410em auto 0;
+	margin: 460em auto 0;
 	background-image:linear-gradient(to left, #FFCC00, white 90%);
 	border-top: 8px solid #FFCC00;
 }