Dies ist die Windows-App mit dem Namen 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 einen beliebigen OS OnWorks-Online-Emulator von dieser Website, aber einen besseren Windows-Online-Emulator.
- 5. Rufen Sie vom gerade gestarteten OnWorks Windows-Betriebssystem unseren Dateimanager https://www.onworks.net/myfiles.php?username=XXXXX mit dem gewünschten Benutzernamen auf.
- 6. Laden Sie die Anwendung herunter und installieren Sie sie.
- 7. Laden Sie Wine aus den Software-Repositorys Ihrer Linux-Distributionen herunter. Nach der Installation können Sie dann auf die App doppelklicken, um sie mit Wine auszuführen. Sie können auch PlayOnLinux ausprobieren, eine schicke Schnittstelle über Wine, die Ihnen bei der Installation beliebter Windows-Programme und -Spiele hilft.
Wine ist eine Möglichkeit, Windows-Software unter Linux auszuführen, jedoch ohne Windows. Wine ist eine Open-Source-Windows-Kompatibilitätsschicht, die Windows-Programme direkt auf jedem Linux-Desktop ausführen kann. Im Wesentlichen versucht Wine, genügend Windows von Grund auf neu zu implementieren, damit alle diese Windows-Anwendungen ausgeführt werden können, ohne dass Windows tatsächlich benötigt wird.
SCREENSHOTS
Ad
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.
