CHASE

Contract-based Heterogeneous Analysis and Systems Exploration

CHASE is a framework for requirement capture, formalization, and validation for cyber-physical systems.

Intended Use

CHASE features a modular and extensible software infrastructure that can support different domain-specific languages, modeling formalisms, and analysis tools. It has been applied to industrial design examples, including control of aircraft power distribution networks and arbitration of a mixed-criticality automotive bus.

The CHASE framework components and flow

The front-end modules parse the specification languages and build the CHASE representation of a design problem. The CHASE libraries represent and manipulate systems, behaviors, and contracts. The back-end modules translate the problems into the languages of verification and synthesis tools.

Quick start

The chase repository is the entry point to CHASE: it collects all the modules and builds them at once. The complete CHASE toolchain, including the gr1c, slugs, and nuXmv solvers, is available as a Docker image (nuXmv is free for academic and non-commercial use, and installed only when its license is accepted):

$>  git clone --recursive https://github.com/chase-cps/chase
$>  cd chase
$>  docker build --build-arg ACCEPT_NUXMV_LICENSE=yes -t chase .
$>  docker run --rm -it chase

The container starts in the demos directory. To build CHASE from sources, see Requirements and Installation.

Python package

The chase_cps Python package provides contracts written in the standard LTL syntax, the contract algebra of CHASE (composition, conjunction, merging, quotient, separation, saturation, simplification), and refinement, consistency, compatibility, and realizability checks with nuXmv and slugs. A failed check returns a counterexample trace.

$>  pip install chase-cps

The checks need nuXmv, and slugs for realizability, installed separately with chase-cps install nuxmv --accept-license and chase-cps install slugs (or by hand); chase-cps doctor shows the tools found, and chase-cps check specs.ltl checks the contracts of a specification from the command line.

from chase_cps import Contract, refines

spec = Contract.from_strings(inputs=["req"], outputs=["grant"],
                             assumptions=["G F !req"],
                             guarantees=["G (req -> F grant)"], name="Spec")
impl = Contract.from_strings(inputs=["req"], outputs=["grant"],
                             guarantees=["G (req -> X grant)"], name="Impl")
print(refines(impl, spec).status)

Publications

CHASE has been presented at the IEEE/ACM Design, Automation and Test in Europe (DATE) conference 2018

Pierluigi Nuzzo, Michele Lora, Yishai Feldman, Alberto Sangiovanni-Vincentelli, “CHASE: Contract-Based Requirement Engineering for Cyber-Physical System Design”

To cite CHASE in an academic work, please use the following bibtex entry:

@inproceedings{CHASE:2018:DATE,
  title={CHASE: Contract-based requirement engineering for cyber-physical system design},
  author={Nuzzo, Pierluigi and Lora, Michele and Feldman, Yishai A and Sangiovanni-Vincentelli, Alberto L},
  booktitle={Proceedings of the Design, Automation \& Test in Europe Conference \& Exhibition (DATE) 2018},
  pages={839--844},
  year={2018},
  organization={IEEE}
}

The DATE18 directory of the demos repository contains the specification files used in the experimental section of the paper.

Other publications

CHASE components and repositories

CHASE is organized in the following components, available at the corresponding repositories:

Index

Acknowledgement

We acknowledge the support of the National Science Foundation (awards 1846524 and 2139982), the Office of Naval Research (award N00014-20-1-2258), the Defense Advanced Research Projects Agency (award HR00112010003), the Okawa Foundation, and the European Union’s Horizon 2020 research and innovation program under the Marie Sklodowska-Curie grant agreement No. 894237.