CHESS 1.1.1 has been released! It is a bug-fix version of release 1.1.0.
The key features of the version 1.1.0 are:
- Cross-level contract refinement.
- Support for "timed" time model.
- Improved default user settings.
- Increased tests coverage.
- Used xText editors for textual areas.
- Defined AST for guards/effects on state machines.
- Improved generation and auto-layout of diagrams.
- Created default workspace for V&V analysis.
- Further formal verification of state machine.
- Improved checker manager.
- Fixed Maven warnings.
See links below to download a full Eclipse CHESS distribution and the
model examples.
Java 8 JRE/JDK is mandatory for CHESS.
If you want to install the CHESS plugins by using the
Eclipse update site feature, check the
Getting
Started page For release details, please check the
release plan.
CHESS Eclipse full distribution:
CHESS-1.1.1: Windows 64 bit - Linux 64 bit - MacOS 64 bit
Previous versions:
CHESS-1.0.0: Windows 64 bit - Linux 64 bit - MacOS 64 bit
CHESS-0.1.0: Windows 64 bit - Linux 64 bit
CHESS model examples
Producer-Consumer
(example about schedulability analysis)
IndustrialDrive
(example about schedulability and E2E response time analyses)
Wheel
Braking System (example about contract-based design)
Sense
Spacecraft Rate (example about contract-based design, model checking
and fault tree analysis)
Train Gate Controller (example about model checking with timed model)
Hybrid
Braking System (example about safety analysis with CHESS-FLA and
CHESS-SBA)