This is a pre-production deployment of Warehouse. Changes made here affect the production instance of PyPI (pypi.python.org).
Help us improve Python packaging - Donate today!

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.

Release History

Release History

This version
History Node

0.1.2

History Node

0.1.1

History Node

0.1.0

Download Files

Download Files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

File Name & Checksum SHA256 Checksum Help Version File Type Upload Date
st2smv-0.1.2-py2.py3-none-any.whl (46.5 kB) Copy SHA256 Checksum SHA256 py2.py3 Wheel Mar 8, 2017
st2smv-0.1.2.tar.gz (36.7 kB) Copy SHA256 Checksum SHA256 Source Mar 8, 2017

Supported By

WebFaction WebFaction Technical Writing Elastic Elastic Search Pingdom Pingdom Monitoring Dyn Dyn DNS Sentry Sentry Error Logging CloudAMQP CloudAMQP RabbitMQ Heroku Heroku PaaS Kabu Creative Kabu Creative UX & Design Fastly Fastly CDN DigiCert DigiCert EV Certificate Rackspace Rackspace Cloud Servers DreamHost DreamHost Log Hosting