STPA Verifier

Brought to you by: asimabdulkhaleq, lukasbalzer

Downloads: 4 This Week

Last Update: 2017-06-07

Get an email when there's a new version of STPA Verifier

STPA Verifier is an Eclipse plug-in to verify the STPA safety requirements with model checker tools such as SPIN and NuSMV. The STPA-generated safety requirements are automatically transformed into formal specification in LTL (linear Temporal Logic). The STPA Verifier plug-in fetches all LTL formulae from XSTPA and allows user to load the verification model of system (Promela or SMV Model). Furthermore, STPA verifier provides a configuration view of each model checker (SPIN and NuSMV) to enable user to configure the model checker with necessary parameters. It also allows users to extract the Promela model from C-Code of the software by using the ModeX tool. The tool shows the results of each LTL formula in the table with different values (syntax error, success, failed (counterexample)and incomplete).

Project Samples

STPA Verifier

Project Activity

See All Activity >

Follow STPA Verifier

STPA Verifier Web Site

Other Useful Business Software

$300 Free Credits to Build on Google Cloud Icon

$300 Free Credits to Build on Google Cloud

New customers can spin up VMs, build with AI, and query data at no cost.

Put your $300 in credit toward real workloads, then keep building with free monthly usage for 20+ products. No commitment and no charge until you upgrade.

Start Free

Rate This Project

Login To Rate This Project

User Reviews

Be the first to post a review of STPA Verifier!

Additional Project Details

Registered

2016-05-07

Report inappropriate content

$300 Free Credits to Build on Google Cloud

New customers can spin up VMs, build with AI, and query data at no cost.

Put your $300 in credit toward real workloads, then keep building with free monthly usage for 20+ products. No commitment and no charge until you upgrade.

Start Free

Recommended Projects

Triple-A
Triple-A (Automatic Analysis with Automata) is a full-featured library for (finite) automata written in Java with two powerful analysis tools (dealing with LTL model checking and Presburger arithmetics) and a graphical user interface built around it.
autoCode4
Synthesizing embedded control software from formal specifications
Java GDSII Parser
A GDSII database parser and stream integrity verifier
STPATCGenerator
STPA TCGenerator is a stand-alone tool was developed by Asim Abdulkhaleq to generate the safety-based test cases directly from STPA safety analysis results. STPA TCGenereator parses the STPA file project created in XSTAMPP and the safe behavourial model which is created with Simulink's stateflow editor to automatically generate the SMV model and check the correctness of the safe beahvioural model, eliminate the safe test model and generate safety-based test cases. The STPA TCGenerator tool accepts two files as input: an STPA project with extension haz. or .hazx and a stateflow model as xml file. The STPA TCGenerator parses the XML specifications of the STPA project and stateflow model into the corresponding Java objects by using Java Architecture for XML Binding (JAXB) technology. We implemented a Java library called SMV Generator which contains all necessary methods for transforming the XML specifications of the STPA project and stateflow model into an SMV model. To
A-STPA
STPA support tool