Contract-based Compositional Verification for outsourced Flight Critical Systems

This repository contains links to all the software developed partly (or totally) under the NRA NNX14AI09G. It also contains a subdirectory called papers which includes PDF versions of all publications resulting from this project.

CoCoSim

CoCoSim is an automated analysis and code generation framework for Simulink and Stateflow models. Specifically, CoCoSim can be used to verify automatically user-supplied safety requirements expressed as mode-aware assume-guarantee contracts. Moreover, CoCoSim can be used to generate C and/or Rust code.

• Project repository: https://github.com/coco-team/cocoSim2

• Documentation: Installation, CoCoSim Features, Tutorial Videos

• CoCoSim models: Benchmarks, and Regression Tests

Compiler From CoCoSim IR to Lustre

CoCoSim uses internally a translator from CoCoSim Intermediate Representation of Simulink/StateFlow models to Lustre models. The tool can be used as stand-alone tool, and supports the CoCoSim contract specification blocks.

• Project repository: https://github.com/coco-team/ir2lustre

• Documentation: JSON Intermediate Representation of CoCoSim models, and its translation to Lustre

Kind 2

Kind 2 is multi-engine SMT-based model checker for Lustre programs. It is one of the back-end solvers supported by CoCoSim to verify Lustre models.

• Project repository: https://github.com/kind2-mc/kind2

• Website: http://kind2-mc.github.io/kind2/

• Kind 2 web interface: http://kind.cs.uiowa.edu:8080/app/

• Documentation: User documentation, Developer documentation

Teas

Teas is a Test Execution Engine (TEE) compatible with Kind 2's test cases and oracles. It is written in Python, and is able to confront a binary with Kind 2's test cases using an oracle.

• Project repository: https://github.com/kind2-mc/testEAS

• Documentation: Test generation section in Kind 2 User documentation

Zustre

Zustre is a modular SMT-based PDR-style verification engine for Lustre programs. It is also an engine to generate mode-aware assume-guarantee style formal contract. It is one of the back-end solvers supported by CoCoSim to verify Lustre models.

• Project repository: https://github.com/coco-team/zustre

• Documentation: Compilation, Usage, Demo

JDart

JDart is a tool for performing concolic execution on a Java program. It is written as an extension to NASA Java Pathfinder (JPF).

• Project repository: https://github.com/psycopaths/jdart

• Documentation: Installation, Usage

SeaHorn

SeaHorn is a fully automated verification framework for LLVM-based languages.

• Project repository: https://github.com/seahorn/seahorn

• Website: http://seahorn.github.io

• Documentation: Installation, Usage

Log2Model

Log2Model is a framework for reasoning on behaviors in log files.

• Project repository: https://github.com/coco-team/log2model

• Documentation: Installation, Usage, Implementation