Complete features.html.
Change-Id: I13a3ba3a313d24ba5bbe57d1e76f3b6c3ad54faf
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;
}
