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
One Monitoring Tool for IT, OT and Cloud | Free Trial Icon
One Monitoring Tool for IT, OT and Cloud | Free Trial

Vendor-agnostic monitoring across on-prem servers, cloud platforms and OT devices, all in one dashboard. No more tool sprawl.

Modern infrastructure spans data centers, cloud platforms and factory floors, and every blind spot between them is a risk. PRTG supports SNMP, WMI, SSH and other standard protocols to monitor IT, OT and hybrid environments through one customizable dashboard. Build the views your team needs, from network health to application performance, without switching tools. Try PRTG free for 30 days now.
Try PRTG 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