Contract-based Heterogeneous Analysis and Systems Exploration
The framework requires the following third party software in order to be built and executed:
The framework mostly relies on the C++11 Standard and should be portable to any architecture and operating system supporting it. However, due to external dependencies, CHASE is tested on:
third_party/directory of the CHASE release. To install the furnished version of ANTLR4, please refer to the Readme file in the antlr4 release available in the third party directory.
However, it should be sufficient to run the install-deps script in the main chase project directory:
$> sh install-deps.sh
$> export CHASE_COMPILER=compiler
$> export CHASE_COMPILER=clang++
to use Clang rather than GCC.
The compilation is based on GNU Make. The
Makefile is located in the main directory of the release. Use the command:
which creates two executables in the
chase: takes as input a problem expressed using the CHASE formal specification language, creates an internal representation of the specification as a contract, checks the contract consistency (realizability of the specification) and produces a design artifact (e.g., a finite automaton representing the discrete control protocol) if the contract is consistent.
epstool: provides a demonstration of the capabilities of CHASE (a small example of contract-based requirement engineering) specifically targeted to an aircraft Electric Power System (EPS).
It is possible to clean the generated binary files through the command:
$> make clean
Documentation requires Doxygen. The Doxyfile is in
doc/Doxyfile. The Makefile defines a target to build the API documentation:
$> make dox
It will generate HTML and LaTeX documentation in
N.B.: The use of the target
clean will also delete the documentation.