This is the Windows app named VeriSiMPL whose latest release can be downloaded as VeriSiMPL_Version3-0.tar.gz. It can be run online in the free hosting provider OnWorks for workstations.
Download and run online this app named VeriSiMPL with OnWorks for free.
Follow these instructions in order to run this app:
- 1. Downloaded this application in your PC.
- 2. Enter in our file manager https://www.onworks.net/myfiles.php?username=XXXXX with the username that you want.
- 3. Upload this application in such filemanager.
- 4. Start any OS OnWorks online emulator from this website, but better Windows online emulator.
- 5. From the OnWorks Windows OS you have just started, goto our file manager https://www.onworks.net/myfiles.php?username=XXXXX with the username that you want.
- 6. Download the application and install it.
- 7. Download Wine from your Linux distributions software repositories. Once installed, you can then double-click the app to run them with Wine. You can also try PlayOnLinux, a fancy interface over Wine that will help you install popular Windows programs and games.
Wine is a way to run Windows software on Linux, but with no Windows required. Wine is an open-source Windows compatibility layer that can run Windows programs directly on any Linux desktop. Essentially, Wine is trying to re-implement enough of Windows from scratch so that it can run all those Windows applications without actually needing Windows.
SCREENSHOTS
Ad
VeriSiMPL
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.
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)
Audience
Science/Research, Education, Engineering
Programming Language
MATLAB, Java
Categories
This is an application that can also be fetched from https://sourceforge.net/projects/verisimpl/. It has been hosted in OnWorks in order to be run online in an easiest way from one of our free Operative Systems.
