VeriSiMPL Icon

VeriSiMPL

Verification via biSimulations of Max-Plus-Linear models

0 Downloads (This Week)
Last Update:
Download VeriSiMPL_Version3-0.tar.gz
Browse All Files
Windows Mac Linux

Screenshots

Description

This toolbox is used to generate finite abstractions of autonomous Max-Plus-Linear (MPL) systems over R^n. Abstractions are characterized as finite-state Labeled Transition Systems (LTS). The LTS finite abstractions are shown to either simulate or to bisimulate the original MPL system. LTS models are to be verified against given specifications expressed as formulae in Linear Temporal Logic (LTL) and Computation Tree Logic (CTL). The toolbox intends to leverage the NuSMV model checker. Models are to be expressed in the C++ language. The abstraction procedure runs in C++. The generated LTS is exported to the NuSMV language. As such, it can be fed, along with a specification of interest, to the NuSMV model checker.

If you are more familiar with JAVA language, we suggest you to try VeriSiMPL version 2.0 which is fully based on JAVA.

If you are more familiar with MATLAB language, we suggest you to try VeriSiMPL version 1.4 which is fully based on MATLAB.

VeriSiMPL Web Site

Features

  • Generate finite-state LTS abstraction from an MPL system using list and tree data structure
  • Generate Piece-wise Affine representation from an MPL system
  • Verify an MPL system against an LTL or CTL formula
  • Visualize the TS in Graphviz (Version 1.4)
  • Export autonomous model to PWA system in MPT structure (Version 1.4)
  • Reachability analysis of MPL systems (Version 1.4)
  • GUI for abstraction and verification of autonomous MPL systems (Version 1.4)
  • GUI for forward reachability of autonomous MPL systems (Version 1.4)

KEEP ME UPDATED

Other Useful Business Software

The Leading Provider of Business VoIP Phone Systems Icon

Award-Winning Business VoIP Phone System

The Leading Provider of Business VoIP Phone Systems Icon
1 of 5 2 of 5 3 of 5 4 of 5 5 of 5
62 Reviews
  • Unlimited Calling, Faxing, Video Conferencing
  • 24/7 U.S Based Customer Support
  • Super Reliable, Simple to Use

Additional Project Details

Intended Audience

Science/Research, Education, Engineering

Programming Language

MATLAB, Java

Registered

2013-01-07

Thanks for helping keep SourceForge clean.

Screenshot instructions:
Windows
Mac
Red Hat Linux   Ubuntu

Click URL instructions:
Right-click on ad, choose "Copy Link", then paste here →
(This may not be possible with some types of ads)

More information about our ad policies
X

Briefly describe the problem (required):

Upload screenshot of ad (required):
Select a file, or drag & drop file here.

Please provide the ad click URL, if possible:

Get latest updates about Open Source Projects, Conferences and News.

No, thanks