README

Contents of this directory:

README: This file

COPYRIGHT: The content in file COPYRIGHT applies to ALL files (recursively) inside this directory except the hybridsal2xml subdirectory. Files in that directory inherit the SAL licence.

INSTALL.txt: Instructions for installing the software

Makefile: Makefile

src/ : Source code of the relational abstractor for hybrid systems

modelica2hsal/ : A tool for converting Modelica XML models into HybridSal

examples/ : Examples The examples are written as .hsal The relational abstractor AUTOMATICALLY constructs .hasal and .sal .hsal : HybridSAL specification of the hybrid system .hasal: Augmented HybridSAL (original + abstraction) .sal: SAL file containing abstraction of .hsal

hybridsal2xml/ : This directory contains code that parses a HybridSAL (or Augmented HybridSAL file) and creates an XML for it.

How to run the tool?

After installing (see file INSTALL.txt), you can use the tool by (A) Running an existing example, such as, bin/modelica2sal modelica2hsal/examples/RCEngine.xml modelica2hsal/examples/context-property.xml

Or, you can build your own model: (1) Build a .hsal model (see examples in examples/.hsal) Suppose you create examples/mytest.hsal (2) From this directory, run the command: make examples/mytest.sal This should create the file examples/mytest.sal -- which is a relational abstraction of the file examples/mytest.hsal (3) Analyze examples/mytest.sal using SAL model checkers. For Step~(3), you need to download and install SAL tools (http://sal.csl.sri.com). Once installed, you can verify examples/mytest.sal using the command (given from inside the subdirectory examples/): sal-inf-bmc -d 5 mytest where is the name of the property inside the file mytest.hsal For detailed explanation on ONE small example, see the document doc/hsal-ra-report.pdf

How to run the demo?

make RCEngineFull will run the full tool on an example Modelica XML file.

python cc2hsal/src/cc_modelica_hra_verifier.py cc2hsal/examples/SimplifiedShiftControllerDecl.xml modelica2hsal/examples/SDT_OM_Cyber_dss.xml python cc2hsal/src/cc_modelica_hra_verifier.py cc2hsal/examples/SimplifiedShiftControllerDecl.xml modelica2hsal/examples/SDT_OM_Cyber_dss.xml --mapping modelicaURI2CyPhyMap.json python cc2hsal/src/cc_modelica_hra_verifier.py cc2hsal/examples/SimplifiedShiftControllerDeclold.xml modelica2hsal/examples/sdt_om_cyber_dss_old.xml --mapping sdt_om_cyber_dss_old.json python cc2hsal/src/cc_modelica_hra_verifier.py cc2hsal/examples/SimplifiedControllersCyber_before.xml modelica2hsal/examples/SystemDesignTest-r663.xml --mapping modelicaURI2CyPhyMap_r663.json

Some Simple Examples

The Linear*.hsal files contain some simple examples. bin/hsal2hasal examples/Linear1.hsal This creates examples/Linear1.sal sal-inf-bmc -i -d 2 Linear1 correct This model checks the property. It fails to find a violation, but also fails to prove it. sal-inf-bmc -i -d 2 -l helper Linear1 correct Using the helper lemma, the model checker is able to prove the property. sal-inf-bmc -i -d 2 Linear1 helper The helper lemma is itself successfully proved.

The following commands will verify properties of Linear5.hsal bin/hsal2hasal examples/Linear1.hsal cd examples sal-inf-bmc -i -d 3 Linear5 correct

Blood Glucose (incomplete)

Relationally abstract a 8-dimensional blood glucose system: bin/hsal2hasal examples/BGL.hsal The model is incomplete and lacking dynamics of Insulin, insulin-injection controller, and a verification property.

Navigation Examples:

The navigation examples are present in files nav*.hsal nav01b models the different squares in the grid as different components. HybridSAL supports compositional modeling -- different components can be modeled as different MODULEs in HybridSAL. bin/hsal2hasal examples/nav01b.hsal cd examples sal-inf-bmc -d 6 nav01b canreach sal-inf-bmc -i -d 6 nav01b correct The first command creates nav01b.sal, the last two runs of sal-inf-bmc check two different properties: one is false and the other is true (and proved by sal-inf-bmc).

The same can be done on nav01.hsal file -- which is the same as nav01b.hsal, but models the entire system as a SINGLE MODULE, rather than as a composition of different MODULES (as done in nav01b.hsal) Irrespective of the modeling style, the analysis time and results are the same. bin/hsal2hasal examples/nav01.hsal cd examples sal-inf-bmc -d 6 nav01 canreach sal-inf-bmc -i -d 6 nav01 correct

Train-Gate-Controller:

The file tgc.hsal contains a model of a train-gate-controller. Note that the discrete behavior of train, gate, and controller are modeled as different MODULES; the continuous behavior (time elapse) is modeled as a separate MODULE; and finally there is one MODULE that enforces the interaction correctly. Thus, tgc.hsal has five modules and the system is a COMPOSITION of these five MODULEs. We can create the relational abstraction, and then verify, using the following commands: bin/hsal2hasal examples/TGC.hsal cd examples sal-inf-bmc -i -d 10 TGC correct sal-inf-bmc -d 10 TGC canreach sal-inf-bmc -d 10 TGC canreach1

RLC Circuit:

A simple model of the RLC circuit using three differential equations is presented in RLC.hsal bin/hsal2hasal -o examples/RLC.hsal cd examples sal-inf-bmc -i -d 5 RLC ibounded sal-inf-bmc -d 5 RLC canreach Analyzing the RLC circuit at certain sampling times: bin/hsal2hasal -t 0.005 examples/RLC.hsal cd examples sal-inf-bmc -i -d 5 RLC ibounded sal-inf-bmc -i -d 5 RLC canprove sal-inf-bmc -d 8 RLC canreach

Powertrain

To analyze the powertrain model, run the following commands bin/hsal2hasal -o examples/powertrain.hsal This will create the file examples/powertrain.sal Now model check using the following commands cd examples sal-inf-bmc -d 12 powertrain nochatter This takes about 3 minutes of real time and verifies the 'nochatter' property of powertrain.

Now change the initial condition: increase grade to 0.15 (15% grade). This can be done by changing the constant 0.05 in INITIALIZATION of grade in either powertrain.hsal OR powertrain.sal to 0.15. You will have to reconstruct the powertrain.sal from powertrain.hsal (using bin/hsal2hasal command above) if you only change the .hsal file. Now, re-verify. sal-inf-bmc -d 12 powertrain nochatter You will get a trace that shows violation of the property. This will take about 3 minutes of real time. Note that we can analyze the property for a range of initial conditions using just ONE run.

Other simple examples:

Simple Thermostat: SimpleThermo4.hsal Other linear continuous dynamical systems: Linear*.hsal See doc/hsal-ra-report.pdf for explanation of the working of the relational abstractor on the example examples/Linear1.hsal

Contact: Ashish Tiwari