Skip to content

Latest commit

 

History

History
180 lines (125 loc) · 8.21 KB

README.md

File metadata and controls

180 lines (125 loc) · 8.21 KB
Raw

#S3CAMX: S3CAM + Symbolic Execution

S3CAM uses simulations and symboolic execution to find falsifications to safety properties of Hybrid Systems. Please refer to the below publications for details:

  • Zutshi, Sankaranarayanan, Deshmukh, Jin. "Symbolic-Numeric Reachability Analysis of Closed-Loop Control Software" Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control. ACM, 2016.

  • Zutshi, Deshmukh, Sankaranarayanan, Kapinski. "Multiple shooting, cegar-based falsification for hybrid systems." Proceedings of the 14th International Conference on Embedded Software. ACM, 2014.

##Overview The S3CAMX package implements both S3CAMX and S3CAM algorithms.

##Dependencies

S3CAMX is written in Python 2.7, and depends on several python packages. Additionally, the S3CAMX algorithm requires Z3 and symbolic paths generated by Pathcrawler. Matlab and Simulink are required if the given system under test is implemented using them. S-Taliro is required only to compare and reproduce the results in the paper. These dependencies are listed below.

  • Python 2.7.x and its packages. Not required if using Package A.
  • MATLAB R2015b (and Simulink): required to simulate systems which use Matlab based simulators: AFC.
  • Pathcrawler output: Pre-computed symbolic paths required for symbolic execution.
  • Z3: Required for running symbolic execution of the controller (included in Package A).
  • S-Taliro 1.6: Needed to reproduce comparison results (included in Package A).

Distributions

The distribution package was tested on Ubuntu 12.04 and 14.04 and should work on Python 2.7.x (Python 2.7.3 and higher).

We provide two packages of S3CAMX

  • Package A (recommended): pre-compiled frozen package built using cx_freeze.
  • Package B: contains all required sources.

###Installing from Package A (not yet available)

Package A is a pre-compiled distribution and does not require the installation of Python or its packages including Z3. However, Matlab + Simulink and S-Taliro still need to be installed. It is recommended that the user tries to run this before moving on to Package B. The package has been tested with a fresh install of Ubuntu 14.04, but a library mismatch can cause unexpected behavior, in which case a fallback to Package B is advised. In case package A is being used, skip to Installing MATLAB.

###Installing from Package B (this github repository) This package contains only sources and requires the user to compile and obtain the necessary dependencies. ##Installation

###Installing Python and Required Packages

  1. Install Python 2.7.x

Note: The Python build must be configured with the option --enable-shared. This is not the case with the default Python installation found in both Ubuntu 12.04 and hence a different local installation is required. This is only needed to interface Matlab with Python [Matlab -> Python], which is used to generate test results by S-Taliro on systems with simulators in Python. For more details, refer to: --enable-shared

e.g. if using pyenv, then CONFIGURE_OPTS must be set as below


`export CONFIGURE_OPTS='--enable-shared --enable-unicode=ucs4'`
before issuing
`pyenv install 2.7.x`

  • Update Repository
    sudo apt-get update

  • Install basic dependencies
    sudo apt-get install build-essential python-dev

  • pip
    Download get-pip.py and install using
    sudo python ./get-pip.py

  • pyparsing
    sudo -H pip install pyparsing

  • numpy 1.10.4

    • Install or upgrade numpy.
      sudo -H pip install numpy --upgrade
    • Install dependencies: If the above step gives an error due to missing dependencies, then either the user can manually resolve them or use sudo apt-get build-dep python-numpy to install an exhaustive list.

  • scipy 0.16.1

    • Install or upgrade scipy.
      sudo -H pip install scipy --upgrade
    • If the above step gives an error due to missing dependencies, (usually blas, and gfortran) they can be installed using sudo apt-get install libatlas-base-dev gfortran. If this does not work then an exhaustive list can be installed using sudo apt-get build-dep python-scipy

  • blessings
    `sudo -H pip install blessings

  • networkx
    `sudo -H pip install networkx

  • matplotlib 1.5.1

    • Install or upgrade matplotlib
      sudo -H pip install matplotlib --upgrade
    • In the case of unresolved dependencies try to install the commonly missing packages: libfreetpy and libpng
      sudo apt-get install libpng-dev libfreetype6-dev
      Else, use the below for an exhaustive resolution
      sudo apt-get build-dep python-matplotlib

  • tqdm
    sudo -H pip install tqdm

  • sh
    sudo -H pip install sh

###Installing Git sudo apt-get install git

Installing MATLAB

  • MATLAB R2015b or higher.
    The below toolboxes may be required:
    • Simulink: required for running example AFC
    • Optimization toolbox: required for running S-Taliro for comparison

Note: The version R2015b is required and earlier versions will not work due to missing features.

S3CAMX uses both MATLAB -> Python and Python -> MATLAB interface for running S-Taliro on systems based on Python simulators and for analyzing systems based on MATLAB simulator respectively. These two interfaces are provided by MATLAB and can be set up as follows.

Setting up MATLAB -> Python

References:

Setting up Python -> MATLAB

Reference: MATLAB Engine for Python

Installing the Rest

Install Z3, S-Taliro and Pathcrawler using their respective instructions.

Obtaining the Sources

Get py2z3 and S3CAMX (branch: conf_pub).

  • py2z3
    git clone https://github.com/zutshi/py2z3.git
  • S3CAMX
    git clone https://github.com/zutshi/S3CAMX.git
    git checkout conf_pub

Pathcrawler

Pathcrawler Installation and Setup

Please refer to the provided documentation.

Running Pathcrawler

Each system in the Pathcrawler directory contains a script run.sh to generate the trace required to run S3CAMX. The bash script generate_symbolic_paths.sh can be used to generate the traces for every system in the examples folder.

RUNNING S3CAMX

  • To configure paths, please modify

    • set_path.sh and update the paths for Z3's Python bindingd and py2z3.
    • staliro_add_path.m and update the path for S-Taliro.

  • Compile each system's controller by running
    compile_examples.sh

  • Start and share minimal Matlab session (optional): - Open a terminal and type matlab& -nojvm -nodisplay -nosplash - In Matlab, type the below to share the matlab engine matlab.engine.shareEngine('<engine_name>')

  • To simulate a system run, use ./secam.py -f <system path> -s <number of simulations>

  • To run S3CAM, use ./secam.py -f <system path> -c

  • To run S3CAMX, use ./secam.py -f <system path> -x pathcrawler -r trace -t tree

  • A shared Matlab engine can be provided as below. ./secam.py -f <system path> [options] --meng <engine_name> This engine will be used to simulate systems which use Matlab simulators. If it is not provided, a Matlab engine will be started. A shared engine is preferred as launching a new Matlab engine is time consuming.

[http://tmpvar.com/markdown.html]