| <!doctype html> | |
| <html> | |
| <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" /> | |
| </head> | |
| <body> | |
| <header> | |
| <div class="logo-left width"> | |
| <a href="index.html"><img src="images/logo_chess_350.gif" | |
| alt="CHESS logo" width=""></a> | |
| </div> | |
| </header> | |
| <nav> | |
| <div class="width"> | |
| <ul> | |
| <li class="start"><a href="index.html">Home</a></li> | |
| <li class="divider-vertical-second-menu"></li> | |
| <li class="selected"><a href="features.html">Features</a></li> | |
| <li class="divider-vertical-second-menu"></li> | |
| <li><a href="start.html">Getting Started</a></li> | |
| <li class="divider-vertical-second-menu"></li> | |
| <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> | |
| </div> | |
| </nav> | |
| <div id="hrdiv"> | |
| <img src="images/bg_breadcrumb.jpg" width="" alt="" height="" /> | |
| </div> | |
| <div id="body" class="width-started"> | |
| <article class="expanded"> | |
| <ul class="tabs"> | |
| <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> | |
| <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%" class="center"/></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%" class="center"/></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%" class="center"/></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%" class="center"/></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%" class="center"/></a> | |
| <div class="caption">Figure 5: Analysis View</div> | |
| </p> | |
| <p> | |
| <h3>Contract-based design</h3> | |
| <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>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 | |
| 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%" class="center"/></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></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%" class="center"/></a> | |
| <div class="caption">Figure 7: Schedulability Analysis | |
| Report</div> | |
| <p></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%" class="center"/></a> | |
| <div class="caption">Figure 8: Transformation chain</div> | |
| <p></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">System-Level Design</label> | |
| <div id="tab-content2" class="tab-content"> | |
| <h2>System Design</h2> | |
| <h3>System Definition</h3> | |
| <h4>Requirements Specification</h4> | |
| <p>Requirements can be represented in the model by using the | |
| SysML standard support, i.e. by using the Requirements Diagram | |
| and Requirement SysML construct. CHESS comes with a dedicated | |
| view/package called “RequirementView”, where the SysML | |
| Requirement Diagram and then the requirements can be created. | |
| Requirements available in the CHESS model can then be linked to | |
| other architectural entities by using the standard SysML support, | |
| so in particular by allocating requirements to components using | |
| the Satisfy relationships.</p> | |
| <h4>System Component Definition</h4> | |
| <p>During this activity, the architecture of the system, i.e. | |
| its constituent components and their relationships, is produced. | |
| The definition of the system architecture foresees the design of | |
| components in isolation, i.e. components designed out of any | |
| particular context (to exploit their reuse), or the | |
| identification (reuse) of the components from existing | |
| libraries/models. The hierarchical modelling of the entire system | |
| architecture is supported to be able to manage the complexity of | |
| the system itself, where the hierarchy can be obtained by using a | |
| top-down or bottom-up design process, where the later in | |
| particular can be realized by following a design by reuse | |
| approach.</p> | |
| <p>A component must come with typed input/output ports | |
| representing the boundary of the component itself, where ports | |
| represent interaction points through which the component can | |
| exchange information with the context. It is worth noting that | |
| the modelling of the component boundary cannot be limited to the | |
| identification of the input/output ports of the component itself; | |
| additional information about the possible (functional and | |
| extra-functional) behaviours of the component and the expected | |
| behaviours of the context must be provided, e.g. to be able to | |
| evaluate if a given component can collaborate in a given | |
| scenario. This relevant part of the specification of the | |
| component boundary can be performed by using the contract-based | |
| approach. When a component has been defined, then it can be | |
| instantiated as part of the given system under design and | |
| connected to the other instances already identified.</p> | |
| <p>The system is modelled, i.e. it is decomposed, as a | |
| collaboration of instances of components. The decomposition of | |
| the architecture can proceed at any level, i.e. a system | |
| component can be also decomposed, according to its complexity. | |
| Different instances of the same component (and different ports | |
| with the same type) can be represented as a single instance with | |
| multiplicity greater than 1. SysML, the OMG general-purpose | |
| modelling language for systems engineering, is proposed in CHESS | |
| for the modelling of the system and its constituent components. | |
| In particular, SysML Block Definition Diagram is used to model | |
| the system and its components, while a SysML Internal Block | |
| Diagram can be associated to the system or component and used to | |
| model its input/output ports, its decomposition into parts and | |
| how the parts are connected.</p> | |
| <h3>Requirements Formalization</h3> | |
| <p>This activity has the goal of translating the informal | |
| requirements allocated to system components into formal | |
| properties. Formal properties are textual expressions specified | |
| in a restricted grammar so that their semantics is formally | |
| defined (in rigorous mathematical terms). Such expressions refer | |
| to the elements of the system component interface defined in the | |
| previous activity. CHESS supports the specification of | |
| well-formed formal properties with the help of an automated | |
| completion feature that suggests the possible continuations of a | |
| partial specification. Formal properties can be further | |
| structured into contracts.</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%" class="center"/></a> | |
| <div class="caption">Property Editor with “completion | |
| assistance”</div> | |
| <h3>Requirements Early Validation</h3> | |
| <p>This validation is done by checking if a specific guarantee | |
| of the contract satisfies the assumption of another contract.</p> | |
| <h3>Functional Refinement</h3> | |
| <p>The architectural refinement defines in detail how the | |
| different parts of the system are connected and interact to | |
| fulfill the system requirements. To refine the architecture, the | |
| sub-requirements and sub-components of the system must be | |
| identified. Allocation of requirements/sub-requirements to | |
| sub-components must be managed, as well as formalization of | |
| sub-requirements. In case of reuse of components (as | |
| sub-components), associated satisfied requirements and | |
| implemented contracts are reused. Information about requirements | |
| refinement can be managed in CHESS by using the SysML standard | |
| support.</p> | |
| <h4>Parameters and Configurations</h4> | |
| <p>The parameterization of an architecture is the procedure to | |
| define and use a (possibly infinite) set of parameters to set the | |
| number of components, the number of ports, the connections, and | |
| the static attributes of components. The instantiation of an | |
| architecture is the procedure to assign the values of the | |
| parameters used in the input parameterized architecture. The | |
| outcome is an architecture with a fixed number of components, | |
| ports, connections, and static attributes of components.</p> | |
| <h4>Contract Refinement</h4> | |
| <p>The contract refinement requires one prior phase, the | |
| definition of the contract. Contracts refinement must follow the | |
| requirements refinement. Indeed, a contract is implicitly linked | |
| to the formalized requirements (via its assumption and guarantee | |
| properties); so, the requirements referred by contracts appearing | |
| in a refinement relationship should also have a corresponding | |
| refinement traced.</p> | |
| <h3>Component’s Nominal and Faulty Behaviour Definition</h3> | |
| <p>System component static definition, i.e. its properties, | |
| ports, contracts, can be enriched with behavioural models by | |
| means of UML state machine diagrams. In CHESS, state machine | |
| diagrams can be used to model the nominal and the faulty | |
| behaviour of the component. Nominal state machine are basically | |
| standard UML ones. In CHESS, by using a subset of the UML support | |
| for state machine modelling, it is also possible to use model | |
| transformation to automatically generate an SMV (the input | |
| language of nuXmv) representation of the modelled nominal state | |
| machines, together with the components structure definition (this | |
| is then used to perform automatic generation of fault tree. In | |
| nominal state machines, each transition comes with a guard and an | |
| effect. The guard is a boolean condition upon the values of | |
| 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%" class="center"/></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 | |
| dependability profile enables dependability architects to model | |
| dependability information necessary to conduct dependability | |
| analysis, basically by allowing the modelling of failure modes | |
| and criticality, the failure behaviours for a component in | |
| isolation (so how events can lead to components failure modes) | |
| and the failure modes propagation between connected components | |
| (via components ports).</p> | |
| <h3>Functional Early Verification</h3> | |
| <h4>Contract-Based Verification of Refinement</h4> | |
| <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> | |
| <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%" class="center"/></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> | |
| <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> | |
| <p>As a further verification step, CHESS enables to verify | |
| whether the behavioural specification of the system, specified by | |
| state machines, is compliant with the contract specification.</p> | |
| <p> | |
| <a id="figure3"><img | |
| style="background: #fff; box-shadow: 0px 0px 6px #111;" | |
| alt="An example of the result of the check contract implementation shown in the “Trace” view. " | |
| src="images/contract-implementation.png" width="85%" class="center"/></a> | |
| <div class="caption">An example of the result of the check | |
| contract implementation shown in the “Trace” view. It is possible | |
| to see that four contracts are not satisfied by the state | |
| machines of their associated component and one contract not.</div> | |
| <h4>Model Checking</h4> | |
| <p>Besides the verification of contracts, the user may want to | |
| verify other properties on the state machine. The specifications | |
| to be checked on the FSM can be expressed in temporal logics like | |
| Computation Tree Logic (CTL), Linear Temporal Logic (LTL) | |
| extended with Past Operators, and Property Specification Language | |
| (PSL) that includes CTL and LTL with Sequential Extended Regular | |
| Expressions (SERE), a variant of classical regular expressions. | |
| It is also possible to analyse quantitative characteristics of | |
| the FSM by specifying real-time CTL specifications.</p> | |
| <p>CTL and LTL specifications are evaluated by nuXmv to | |
| determine their truth or falsity in the FSM. When a specification | |
| is discovered to be false, nuXmv constructs and prints a | |
| counterexample, i.e. a trace of the FSM that falsifies the | |
| property.</p> | |
| <p>There are three possible model checking available:</p> | |
| <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> | |
| <p>The faulty behaviour for a component is provided through a | |
| state machine, the latter tagged with the | |
| <<ErrorModel>> stereotype defined in the CHESS | |
| dependability profile13. In the error model, the information | |
| about the error states can be provided by using the | |
| <<ErrorState>> stereotype. Then, for a given error | |
| 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> | |
| <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%" class="center"/></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 | |
| fault tree generation can be obtained by invoking the xSAP | |
| symbolic model checker through the CHESS environment. Please | |
| refer to the CHESS User Manual for instructions on how to | |
| configure the analysis.</p> | |
| <p>Once the analysis is executed, the fault tree is | |
| automatically shown in a dedicated panel in the frontend. If | |
| fault probabilities have been specified during the configuration | |
| of the error model, the fault tree will report their combination. | |
| 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%" class="center"/></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 | |
| details.</p> | |
| <h3>Contract-Based Safety Analysis</h3> | |
| <p>The contract-based safety analysis identifies the component | |
| failures as the failure of its implementation in satisfying the | |
| contract. When the component is composite, its failure can be | |
| caused by the failure of one or more subcomponents and/or the | |
| failure of the environment in satisfying the assumption. As | |
| result, this analysis produces a fault tree in which each | |
| intermediate event represents the failure of a component or its | |
| environment and is linked to a Boolean combination of other | |
| nodes; the top-level event is the failure of the system | |
| component, while the basic events are the failures of the leaf | |
| 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 | |
| modelling of the system components and the verification, | |
| validation, and analysis results. The generated document is | |
| composed by a list of sections. The first section includes the | |
| diagrams that are not associated to a specific component, such as | |
| the block definition diagrams.</p> | |
| </div></li> | |
| <!--li> | |
| <input name="tabs" id="tab2" type="radio"> | |
| <label for="tab2">Example</label> | |
| <div id="tab-content2" class="tab-content"> | |
| <p>CHESS model example currently not available</p> | |
| <h3>CHESS Model</h3> | |
| <p style="text-align: left; padding:10px;"> | |
| CHESS model example | |
| </p> | |
| </div> | |
| </li> | |
| <li> | |
| <input name="tabs" id="tab3" type="radio"> | |
| <label for="tab3">Videos</label> | |
| <div id="tab-content3" class="tab-content"> | |
| <p>CHESS modeling video currently not available</p> | |
| <h3>CHESS Video</h3> | |
| <p style="text-align: left; padding:10px;"> | |
| CHESS model example | |
| </p> | |
| </div> | |
| </li--> | |
| </ul> | |
| </article> | |
| </div> | |
| <div class="clear"></div> | |
| <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 | |
| Project Page</a></li> | |
| </ul> | |
| <ul> | |
| <li><h4>Legal</h4></li> | |
| <li><a href="http://www.eclipse.org/legal/privacy.php">Privacy | |
| Policy</a></li> | |
| <li><a href="http://www.eclipse.org/legal/termsofuse.php">Terms | |
| of Use</a></li> | |
| <li><a href="http://www.eclipse.org/legal/copyright.php">Copyright | |
| Agent</a></li> | |
| <li><a href="http://www.eclipse.org/org/documents/epl-v10.php">Eclipse | |
| Public License</a></li> | |
| <li><a href="http://www.eclipse.org/legal/">Legal Resources</a></li> | |
| </ul> | |
| <ul> | |
| <li><h4>Useful Links</h4></li> | |
| <li><a | |
| href="https://bugs.eclipse.org/bugs/enter_bug.cgi?product=Chess">Report | |
| a Bug</a></li> | |
| <li><a href="https://wiki.eclipse.org/CHESS">Documentation</a></li> | |
| <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 | |
| 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><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> | |
| <li><a href="http://www.mdh.se/">Mälardalen University</a></li> | |
| </ul> | |
| <table> | |
| <tr> | |
| <td><a href="https://www.yourkit.com"><img | |
| src="images/yklogo.png" alt="YourKit logo" | |
| style="width: 25%; height: 25%"></a> <br /> <font size="2">Thanks | |
| YourKit for providing us free licenses of <a | |
| href="https://www.yourkit.com/java/profiler/">YourKit Java | |
| Profiler</a> | |
| </font></td> | |
| <td> | |
| <div class="right-footer"> | |
| <a href="http://www.eclipse.org/"><img | |
| src="images/eclipse.png" alt="Eclipse logo"></a> <br /> | |
| Copyright ©<span id="year">2016</span> The Eclipse Foundation. <br /> | |
| All Rights Reserved. | |
| </div> | |
| </td> | |
| </tr> | |
| </table> | |
| <div class="clear"></div> | |
| </div> | |
| </footer> | |
| </body> | |
| </html> |