Dies ist die Linux-App namens VeriSiMPL, deren neueste Version als VeriSiMPL_Version3-0.tar.gz heruntergeladen werden kann. Es kann online beim kostenlosen Hosting-Anbieter OnWorks für Workstations ausgeführt werden.
Laden Sie diese App namens VeriSiMPL mit OnWorks kostenlos herunter und führen Sie sie online aus.
Befolgen Sie diese Anweisungen, um diese App auszuführen:
- 1. Diese Anwendung auf Ihren PC heruntergeladen.
- 2. Geben Sie in unserem Dateimanager https://www.onworks.net/myfiles.php?username=XXXXX den gewünschten Benutzernamen ein.
- 3. Laden Sie diese Anwendung in einem solchen Dateimanager hoch.
- 4. Starten Sie den OnWorks Linux-Online- oder Windows-Online-Emulator oder den MACOS-Online-Emulator von dieser Website.
- 5. Rufen Sie vom gerade gestarteten OnWorks Linux-Betriebssystem aus unseren Dateimanager https://www.onworks.net/myfiles.php?username=XXXXX mit dem gewünschten Benutzernamen auf.
- 6. Laden Sie die Anwendung herunter, installieren Sie sie und führen Sie sie aus.
SCREENSHOTS:
VeriSiMPL
BESCHREIBUNG:
Diese Toolbox wird verwendet, um endliche Abstraktionen autonomer Max-Plus-Linear (MPL)-Systeme über R^n zu generieren. Abstraktionen werden als endliche Labeled Transition Systems (LTS) charakterisiert. Es wird gezeigt, dass die endlichen LTS-Abstraktionen das ursprüngliche MPL-System entweder simulieren oder bisimulieren. LTS-Modelle müssen anhand vorgegebener Spezifikationen verifiziert werden, die als Formeln in Linear Temporal Logic (LTL) und Computation Tree Logic (CTL) ausgedrückt werden. Die Toolbox soll den NuSMV-Modellprüfer nutzen. Modelle müssen in der Sprache C++ ausgedrückt werden. Das Abstraktionsverfahren läuft in C++. Das generierte LTS wird in die NuSMV-Sprache exportiert. Daher kann es zusammen mit einer interessierenden Spezifikation dem NuSMV-Modellprüfer zugeführt werden.
Wenn Sie mit der JAVA-Sprache besser vertraut sind, empfehlen wir Ihnen, VeriSiMPL Version 2.0 auszuprobieren, die vollständig auf JAVA basiert.
Wenn Sie mit der MATLAB-Sprache besser vertraut sind, empfehlen wir Ihnen, VeriSiMPL Version 1.4 auszuprobieren, die vollständig auf MATLAB basiert.
Eigenschaften
- Generieren Sie eine LTS-Abstraktion mit endlichen Zuständen aus einem MPL-System mithilfe einer Listen- und Baumdatenstruktur
- Generieren Sie eine stückweise affine Darstellung aus einem MPL-System
- Überprüfen Sie ein MPL-System anhand einer LTL- oder CTL-Formel
- Visualisieren Sie den TS in Graphviz (Version 1.4)
- Autonomes Modell in MPT-Struktur in das PWA-System exportieren (Version 1.4)
- Erreichbarkeitsanalyse von MPL-Systemen (Version 1.4)
- GUI zur Abstraktion und Verifizierung autonomer MPL-Systeme (Version 1.4)
- GUI für Vorwärtserreichbarkeit autonomer MPL-Systeme (Version 1.4)
Publikum
Wissenschaft/Forschung, Bildung, Ingenieurwesen
Programmiersprache
MATLAB, Java
Kategorien
Dies ist eine Anwendung, die auch von https://sourceforge.net/projects/verisimpl/ abgerufen werden kann. Es wurde in OnWorks gehostet, um es auf einfachste Weise online über eines unserer kostenlosen Betriebssysteme ausführen zu können.