A tool to convert Structured Text PLC code to an SMV model.
Project description
Overview
st2smv
is a tool for converting programmable logic controller (PLC)
code to a formal model, and checking whether the model satisfies
various properties (e.g., temporal logic specifications). As its name
implies, st2smv
can process PLC code written in a subset of the
Structured Text (ST) programming language, and produces models in the
SMV language.
Basic Use
Run the command
st2smv --help
to see a summary of how to use st2smv
.
Consider the following ST program with 3 boolean variables:
x1 := x2;
x2 := NOT x1;
x3 := NOT (x1 = x2);
and the specification
SPEC AG(x3);
To convert the file code.st
to a model, run the command
st2smv --convert --input code.st --output-directory outdir
where outdir
is the directory where you want to save the output.
You should now have the following files:
.
├── code.st
├── outdir
│ ├── ast.json
│ └── model.json
└── spec.smv
ast.json
contains the abstract syntax tree (AST) of the code, and
model.json
is the model, stored in an intermediate representation.
To produce an SMV model (including the specification), run the command
st2smv --combine --input outdir/model.json spec.smv | tee outdir/model.smv
which will print the model and write it to the file outdir/model.smv
.
Finally, run the command
NuSMV outdir/model.smv
to check the specification (which is true).
Structure of the Model
In progress…
Advanced Use
In progress…
Installation
To install st2smv
from the Python Package Index (PyPI), run the
command
pip install st2smv
If you have instead obtained this package from another source and wish to install that copy, run the command
pip install st2smv_directory
where st2smv_directory
is the location of this directory (i.e., the
directory that contains the file setup.py
).
Dependencies
st2smv
converts PLC code to a formal model, which then must be
analyzed using a solver. The current version of st2smv
produces
models that can be analyzed using
SynthSMV, which must be
installed separately. NuSMV (which SynthSMV
is based on) can be used to check some, but not all, of the models
that st2smv
produces.
License
GPLv3+: The GNU General Public License, version 3, or (at your option) any later version.
Project details
Release history Release notifications | RSS feed
Download files
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.
Source Distribution
Built Distribution
Hashes for st2smv-0.2.0rc1-py2.py3-none-any.whl
Algorithm | Hash digest | |
---|---|---|
SHA256 | 94a175d16c4e0fc775141889354e06efff8289d5b3dc0a64c2f8d67e4ca0973c |
|
MD5 | 11cb9d2abdbd1ce7a5c5c574b8d032fe |
|
BLAKE2b-256 | 4caabe417e45c450bf970de9e434cd61ff5b8f507d492a434dcb5d400c6be8f6 |