<!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
							&lt;&lt;ErrorModel&gt;&gt; stereotype defined in the CHESS
							dependability profile13. In the error model, the information
							about the error states can be provided by using the
							&lt;&lt;ErrorState&gt;&gt; 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>