CoCoSim v1.0

Author: hbourbouh

Dockerfile

@@ -0,0 +1,74 @@
+FROM ubuntu:18.04 as builder
+
+
+# Install build dependencies
+RUN apt-get update && apt-get install -y \
+    automake \
+    autoconf \
+    libtool \
+    git \
+    pkg-config \
+    unzip \
+    wget
+
+RUN git clone --depth=1 --branch develop https://github.com/kind2-mc/kind2.git  kind2-build
+RUN git clone --depth=1 --branch master https://cavale.enseeiht.fr/git/lustrec  lustrec-build
+
+# Install opam and ocaml from GitHub (Ubuntu version causes problems)
+RUN wget -qq https://github.com/ocaml/opam/releases/download/2.0.1/opam-2.0.1-x86_64-linux \
+  && mv opam-2.0.1-x86_64-linux /usr/local/bin/opam && chmod a+x /usr/local/bin/opam \
+  && opam init --disable-sandboxing --yes --comp 4.04.0 && eval $(opam env)
+
+# Install ocaml packages needed for Kind 2.
+RUN opam install --yes ocamlfind camlp4 menhir ocamlgraph cmdliner fmt logs num yojson
+
+# Force to use opam version of ocamlc.
+ENV PATH="/root/.opam/4.04.0/bin:${PATH}"
+
+
+
+# Retrieve Z3 binary
+RUN wget -qq https://github.com/Z3Prover/z3/releases/download/z3-4.7.1/z3-4.7.1-x64-ubuntu-16.04.zip \
+ && unzip z3-4.7.1-x64-ubuntu-16.04.zip
+
+# Retrieve Yices 2
+RUN wget -qq http://yices.csl.sri.com/releases/2.6.0/yices-2.6.0-x86_64-pc-linux-gnu-static-gmp.tar.gz \
+ && tar xvf yices-2.6.0-x86_64-pc-linux-gnu-static-gmp.tar.gz
+
+# Retrieve JKind and CVC4 (required for certification)
+RUN wget -qq https://github.com/agacek/jkind/releases/download/v4.0.1/jkind.zip && unzip jkind.zip \
+ && ./kind2-build/docker_scripts/latest_cvc4.sh
+
+# Build Lustrec
+WORKDIR lustrec-build
+RUN  autoconf && ./configure --prefix=/ && make && make install
+
+# Build Kind 2
+WORKDIR ../kind2-build
+RUN if [ -f "Makefile" ] ; then make clean \
+  && rm -rf src/_build configure Makefile bin src/Makefile src/kind2.native \
+  && autoreconf ; fi
+RUN ./autogen.sh && ./build.sh
+
+
+FROM ubuntu:18.04
+# Install runtime dependencies:
+# JRE (required by JKind) and libgomp1 (required by Z3)
+# Make and gcc for compilation
+RUN apt-get update && apt-get install -y default-jre libgomp1 make gcc\
+  && rm -rf /var/lib/apt/lists/*
+
+COPY --from=builder /z3-4.7.1-x64-ubuntu-16.04/bin/z3 /bin/
+COPY --from=builder /yices-2.6.0/bin/yices-smt2 /bin/
+COPY --from=builder /cvc4 /bin/
+COPY --from=builder /jkind/jkind /jkind/*.jar /bin/
+COPY --from=builder /kind2-build/bin/kind2 /bin/
+COPY --from=builder /lustrec-build/bin/* /bin/
+COPY --from=builder /lustrec-build/include /include/lustrec
+
+# Entry point.
+#ENTRYPOINT ["/bin/kind2"]
+
+WORKDIR /lus
+
+CMD tail -f /dev/null

INSTALL.md

@@ -0,0 +1,98 @@
+
+
+### **Dependencies**
+
+* MATLAB(c) and Simulink version **R2017** or newer (CoCoSim has been well tested in R2017b version)
+
+* [Lustrec](https://github.com/coco-team/lustrec) tool is a modular compiler of Lustre code into C and Horn Clauses. CoCoSim uses lustrec in many features: Test case generation, requirements importation... 
+
+* [Kind2](http://kind2-mc.github.io/kind2/) is a multi-engine, parallel, SMT-based automatic model checker for safety properties of Lustre programs.
+
+<!-- * Formal verification backends: In order to analyse the model, at least one of the following model-checkers should be installed. Currently we support Kind2.
+    * [Kind2](http://kind2-mc.github.io/kind2/) (Supported and highly recommended)
+    * [Zustre](https://github.com/lememta/zustre) (Support in progress)
+    * [JKind](https://github.com/agacek/jkind) (Support in progress) -->
+
+
+
+CoCoSim uses the following external libraries:
+
+* CoCoSim standard libraries from https://github.com/coco-team/cocoSim2
+* Simulink/Matlab selected toolboxes from https://github.com/hbourbouh/cocosim-external-libs
+
+
+### **Installation**
+
+#### Using latest stable version 
+
+We recommend this option. You can download the latest stable version of CoCoSim source code from [here](https://github.com/NASA-SW-VnV/CoCoSim/releases).
+
+CoCoSim is a Matlab Toolbox, in the zip we include the external libraries and binaries for Lustrec and Kind2.
+
+You still need to run the install script to make sure binaries are working on your machine. If not they will be installed from scratch.
+
+In your terminal, go first to `scripts` folder in `cocosim` and run the `install_cocosim` script.
+```
+>cd CoCoSim/scripts
+>./install_cocosim 
+```
+
+The script may require some dependencies, please install them and run the script again.
+
+
+#### Use developer version
+
+1. Clone this cocosim repository in your local machine (develop branch).
+
+2. Download External Matlab Libraries:
+   
+    * Open your Matlab and navigate to `cocosim/scripts` run `install_cocosim_lib(true)` from the Matlab Command window. \
+    Function `cocosim2/scripts/install_cocosim_lib.m` is responsible of copying all required external libraries to the right destination in our repository.
+    It needs `git` to clones external repositories from github and copy some of their code on the
+    right place on CoCoSim.
+    Read function `cocosim2/scripts/install_cocosim_lib.m` to know what are the external libraries are copied to cocosim2 to do it manually in case the function failed for internet connection or `git` issues.
+
+     * Navigate back to `cocosim` then run `start_cocosim` from the Matlab Command window.
+
+3. In your terminal, go first to `scripts` folder in `cocosim` and run the `install_cocosim` script.
+    ```
+    >cd CoCoSim/scripts
+    >./install_cocosim 
+    ```
+
+install_cocosim script assumes the operating system provides:
+    bash, basename, dirname, mkdir, touch, sed, date,
+    cat, rm, mv, cp, ln, find, tee, patch,tar, gzip, 
+    gunzip, xz, make, git
+
+Also the following dependencies:
+autoconf, automake, aclocal, pkg-config.
+
+The script detects the missing dependencies that should be installed by 
+the user.
+
+If the above script failed to install the tools. You may install them in the following paths. If you have linux machin, change `osx` by `linux`.
+
+KIND2 binary: `CoCoSim/tools/verfiers/osx/bin/kind2`
+
+Z3 binary: `CoCoSim/tools/verfiers/osx/bin/z3`
+
+<!-- JKIND binary: `CoCoSim/tools/verfiers/jkind/jkind` -->
+
+<!-- JLUSTRE2KIND binray: `CoCoSim/tools/verfiers/jkind/jlustre2kind` -->
+
+<!-- ZUSTRE binary: `CoCoSim/tools/verfiers/osx/bin/zustre` -->
+
+LUSTREC binary: `CoCoSim/tools/verfiers/osx/bin/lustrec`
+
+LUSTRET binary: `CoCoSim/tools/verfiers/osx/bin/lustret`
+
+LUCTREC_INCLUDE_DIR: `CoCoSim/tools/verfiers/osx/include/lustrec`
+
+
+If you want to customize these paths go to `cocosim/tools/tools_config.m` and change the values of variables KIND2, Z3, <!--JKIND, JLUSTRE2KIND, ZUSTRE, --> LUSTREC, LUSTRET, LUCTREC_INCLUDE_DIR to your preferences.
+
+
+**Quick Start**
+-------------------
+Explanation for each CoCoSim features can be found [here](doc/EXAMPLES.md)

LICENSE.pdf

@@ -1,2 +1,86 @@
-# CoCoSim
-Automated Analysis Framework for Simulink/Stateflow models.
+**CoCoSim: Contract based Compositional verification of Simulink models**
+=====================================================================
+
+[![License](https://img.shields.io/badge/license-NOSA%201.3-blue.svg)](LICENSE.pdf)
+[![Release](https://img.shields.io/badge/release-v1.0-orange.svg)](https://github.com/NASA-SW-VnV/CoCoSim/releases/)
+
+CoCoSim (Contract based Compositional verification of Simulink models) 
+consists of an open architecture, allowing the integration of different analyses. The motivation is to support different verification techniques to scale to large models. The main objective of CoCoSim is to provide the following:
+* A **formal semantic** for a well defined subset of Simulink/Stateflow blocks. This formal representation allows the use of formal verification methods and code generation. It also can be used as a semantic of reference for other tools. Find more about the formal semantics of Simulink/Stateflow used in the [CoCoSim manual](doc/cocosim_user_manual.pdf).
+* A **highly automated** toolchain: all the steps of verification or code generation are automated, check [CoCoSim manual](doc/cocosim_user_manual.pdf).
+* A **Customizable** and **configurable** architecture: Currently CoCosim supports most frequently used Simulink blocks libraries (> 100 blocks) either by transforming them to simpler blocks or by direct translation to a formal language. The translation is customizable and extensible; new blocks can be easily supported.
+* Full **traceability** throughout the analysis process. This traceability is crucial in reporting analysis results expressed in the formal model back to the user in the context of the Simulink model. For instance, the Counter-examples generated by model checkers is reported back to the Simulink level using a Signal Builder block to help the user debug the internal Signals values.
+* **Scalability** to large models: abtained through the use of various verification techniques and compositional reasoning.
+
+CoCoSim can be used to
+verify automatically user-supplied safety requirements. Moreover,
+CoCoSim can be used to generate C and/or Rust code. 
+CoCoSim uses various model checkers for verification (Zustre, Kind2, JKind).
+CoCoSim is currently under development. We welcome any feedback and bug report.
+
+**License**
+-------
+
+CoCoSim has been released under the NASA Open Source Agreement.
+
+**Contact**
+-------
+
+Please contact [email protected] for further information on CoCoSim. Detailed information can be found at the [CoCoSim manual](doc/cocosim_user_manual.pdf)
+
+**Installation**
+---------------
+
+Platforms
+---------
+CoCoSim currently is supported for Mac OS and Linux distributions. Future support is planned for Windows.
+
+Dependancies and Installation instructions can be found [here](INSTALL.md)
+
+**Quick Start**
+-------------------
+
+Explanation for each CoCoSim features can be found [here](doc/EXAMPLES.md)
+
+
+**Release notes and work in progress**
+-------------
+
+For release notes and what actually we are working on see [here](RELEASE_NOTES.md)
+
+**Troubleshooting**
+-------------------
+
+Solution of some common issues with CoCoSim are [here](doc/TROUBLESHOOTING.md)
+
+
+## **Developers**
+
+* Project leader: [Guillaume Brat](https://ti.arc.nasa.gov/profile/brat/) (NASA Ames - USA), [Pierre-Loic Garoche](https://ti.arc.nasa.gov/profile/garoche/) (NASA Ames - USA)
+* Lead Developer: [Hamza Bourbouh](https://ti.arc.nasa.gov/profile/bourbouh/) (NASA Ames - USA)
+
+* Current Contributors: \
+Khanh Trinh (NASA Ames - USA)
+
+* Past Contributors: \
+[Temesghen Kahsai](http://www.lememta.info/), Francois Conzelmann (NASA Ames - USA)
+
+
+**Publications**
+------------
+
+* [Automated analysis of Stateflow models](https://oatao.univ-toulouse.fr/22654/1/bourbouh_22654.pdf)\
+H Bourbouh, PL Garoche, C Garion, A Gurfinkel, T Kahsai, X Thirioux\
+EasyChair 46, 144-161
+
+* [CoCoSim, a code generation framework for control/command applications. An overview of CoCoSim for multi-periodic discrete Simulink models](https://hal.archives-ouvertes.fr/hal-02441334/document)\
+H Bourbouh, PL Garoche, T Loquen, É Noulard, C Pagetti\
+10th European Congress on Embedded Real Time Software and Systems (ERTS 2020)
+
+* [Evaluation of the FRET and CoCoSim tools on the Ten Lockheed Martin Cyber-Physical Challenge Problems](http://www.garoche.net/publication/nasatm-2019-220374/nasatm-2019-220374.pdf)\
+A Mavridou, H Bourbouh, PL Garoche, M Hejase\
+NASA Technial Report: NASA/TM-2019-220374
+
+* Bridging the Gap Between Requirements and Simulink Model Analysis\
+A Mavridou, H Bourbouh, PL Garoche, D Giannakopoulou, T Pressburger, J Schumann\
+REFSQ2020

README.md

@@ -0,0 +1,35 @@
+CoCoSim version 1.0 release notes
+===================================
+
+Release date
+------------
+
+Feb 2020
+
+List of features:
+----------------
+The following is the list of actions the user can call from CoCoSim menu:
+* **Check compatibility** of a model against the CoCoSim compiler from Simulink to Lustre: This will check and report all blocks in the model that are not supported by the compiler. \
+The checking compatibility does not guarantee that the model is fully supported but it detects the blocks/options we already know we do not support.
+You may have other error messages that a specific block is not supported.
+In addition the compatibility is performed for Verification, a model can be supported for verification and not for code generation.
+
+* **Prove properties**: The model should contain requirements to be verified by one of the supported model checkers (currently only KIND2 is integrated). These requirements can be expressed using SLDV verification blocks or CoCoSpec specification blocks (See [CoCoSpec Specification library](https://github.com/coco-team/cocoSim2/blob/master/doc/specificationLibrary.md)). 
+* **Design Error Detection**: Currently cocosim only check for specified minimum and maximum signal values specified by the user on blocks outputs using OutMin and OutMax parameters in blocks dialogue box. The check is done using Kind2 model checker. Future work is planned to support the check of integer overflow, out of bound access array and division by zero.
+This features requires Kind2 to be installed.
+* **Test-case Generation**: Currently cocosim supports:
+    * **Random Testing**: cocosim generates in this case random inputs, a range can be specified by the user using OutMin and OutMax parameters in the Inport block.
+* **Code Generation**: CoCoSim support the generation of C, Lustre and Rust code from a Simulink model.
+
+
+
+
+Features in progress:
+---------------------
+* Support [nuXmv](https://nuxmv.fbk.eu/) model checker.
+* **Check model against guidelines**: This will run the model against a list of guidelines from [NASA - Orion GN&C: MATLAB and Simulink Standards](https://www.mathworks.com/solutions/aerospace-defense/standards/nasa.html).
+
+* **Test-case Generation**: Currently we are working on:
+    * **MC-DC test coverage**: cocosim uses lustret tool to generate MC-DC conditions on the lustre code that will be checked using Kind2. Counterexamples are the test-cases that detects those MC-DC conditions. In the case the condition is not falsified, it means the condition is never activated, therefore a dead logic. 
+    * **Mutation based testing**: cocosim uses lustret tool to generate mutations on the lustre code, a mutation can be a change of arithmetic operator, a relational operator or a constant value. Kind2 is used to find traces that detect those mutations.
+