Google Git
Sign in
eclipse / gerrit / www.eclipse.org / chess / c772254ce53a3139e62dcdb6fe53cb11e6716e64 / . / features.html
blob: 248e4af8786921f07bea81dc63f7de0d04bf58ff [file] [log] [blame]
<!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>