Uppaal Model Checker
http://dbpedia.org/resource/Uppaal_Model_Checker an entity of type: Thing
Uppaal（ウパール）は、形式言語のうち、モデル検査の機能を持つシステム。時間制約付きモデルを図として記述し、検査・検証を行う。時相論理式で検査したい項目を指定する。学術向けは無償利用できるが、商用は有償。日本ではキャッツが販売代理店をしている。JAXAなど、研究開発機関での利用が進んでいる。
rdf:langString
UPPAAL ist ein Model Checker, der an der Universität Uppsala und der Universität Aalborg entwickelt wird. UPPAAL steht für akademische Zwecke kostenlos zur Verfügung. Im Gegensatz zu anderen Model Checkern wie SPIN oder Rebeca erfolgt die Modellierung des Systems nicht hauptsächlich über eine formale Sprache in Textform, sondern durch einen grafischen Editor. In diesem grafischen Editor werden die einzelnen Zustände und die Übergänge zwischen diesen dargestellt. Lokale und globale Variablen sowie einzelne Funktionen werden in einer C-ähnlichen Sprache spezifiziert. Zu überprüfende Eigenschaften werden mit LTL formuliert. Bei kommerzieller Anwendung werden Lizenzgebühren erhoben. UPPAAL wird häufig in der Überprüfung von Algorithmen für Embedded-Systems verwendet.
rdf:langString
UPPAAL è uno strumento software per la verifica di sistemi sistema real-time, modellati sotto forma di reti di . È stato sviluppato a partire dal 1995, in collaborazione tra il Design and Analysis of Real-Time Systems group dell'Università di Uppsala e il Basic Research in Computer Science all'Università di Aalborg; il nome del software deriva dall'unione delle prime tre lettere del nome di ciascuna università. Il tool è usato estensivamente nella ricerca e nello sviluppo di sistemi real-time e l'articolo nel quale il software venne presentato, UPPAAL in a Nutshell, è uno tra i dieci articoli più citati nella storia dell'ingegneria del software.
rdf:langString
UPPAAL is an integrated tool environment for modeling, validation and verification of real-time systems modeled as networks of timed automata, extended with data types (bounded integers, arrays etc.). It has been used in at least 17 case studies since its release in 1995, including on Lego Mindstorms, for the Philips audio protocol, and in gearbox controllers for Mecel. The tool has been developed in collaboration between the Design and Analysis of Real-Time Systems group at Uppsala University, Sweden and Basic Research in Computer Science at Aalborg University, Denmark.
rdf:langString
rdf:langString
UPPAAL
rdf:langString
UPPAAL
rdf:langString
Uppaal
rdf:langString
Uppaal Model Checker
rdf:langString
UPPAAL
rdf:langString
UPPAAL
xsd:integer
697254
xsd:integer
900224894
xsd:date
2014-05-20
xsd:integer
4
rdf:langString
C++ and GUI in Java
rdf:langString
UPPAAL ist ein Model Checker, der an der Universität Uppsala und der Universität Aalborg entwickelt wird. UPPAAL steht für akademische Zwecke kostenlos zur Verfügung. Im Gegensatz zu anderen Model Checkern wie SPIN oder Rebeca erfolgt die Modellierung des Systems nicht hauptsächlich über eine formale Sprache in Textform, sondern durch einen grafischen Editor. In diesem grafischen Editor werden die einzelnen Zustände und die Übergänge zwischen diesen dargestellt. Lokale und globale Variablen sowie einzelne Funktionen werden in einer C-ähnlichen Sprache spezifiziert. Zu überprüfende Eigenschaften werden mit LTL formuliert. Bei kommerzieller Anwendung werden Lizenzgebühren erhoben. UPPAAL wird häufig in der Überprüfung von Algorithmen für Embedded-Systems verwendet. UPPAAL gilt mittlerweile als state-of-the-art Tool und wird für vielfältige wissenschaftliche und industrielle Anwendungen eingesetzt.
rdf:langString
UPPAAL is an integrated tool environment for modeling, validation and verification of real-time systems modeled as networks of timed automata, extended with data types (bounded integers, arrays etc.). It has been used in at least 17 case studies since its release in 1995, including on Lego Mindstorms, for the Philips audio protocol, and in gearbox controllers for Mecel. The tool has been developed in collaboration between the Design and Analysis of Real-Time Systems group at Uppsala University, Sweden and Basic Research in Computer Science at Aalborg University, Denmark. There are the following extensions available:
* Cora for Cost Optimal Reachability Analysis.
* Tron for Testing Real-time systems ON-line (black-box conformance testing).
* Cover for COVERerage-optimal off-line test generation.
* Tiga for TImed GAmes based controller synthesis.
* Port for component based timed systems, exploiting Partial Order Reduction Techniques.
* Pro for PRObabilistic reachability analysis. (Discontinued)
* SMC for Statistical Model Checking.
rdf:langString
Uppaal（ウパール）は、形式言語のうち、モデル検査の機能を持つシステム。時間制約付きモデルを図として記述し、検査・検証を行う。時相論理式で検査したい項目を指定する。学術向けは無償利用できるが、商用は有償。日本ではキャッツが販売代理店をしている。JAXAなど、研究開発機関での利用が進んでいる。
rdf:langString
UPPAAL è uno strumento software per la verifica di sistemi sistema real-time, modellati sotto forma di reti di . È stato sviluppato a partire dal 1995, in collaborazione tra il Design and Analysis of Real-Time Systems group dell'Università di Uppsala e il Basic Research in Computer Science all'Università di Aalborg; il nome del software deriva dall'unione delle prime tre lettere del nome di ciascuna università. Il tool è usato estensivamente nella ricerca e nello sviluppo di sistemi real-time e l'articolo nel quale il software venne presentato, UPPAAL in a Nutshell, è uno tra i dieci articoli più citati nella storia dell'ingegneria del software. Diverse estensioni sono state sviluppate per il tool, tra le quali il supporto per cost optimal reachability analysis, black-box conformance testing, coverage-optimal off-line test generation, timed games based controller synthesis, component based timed systems, statistical model checking.
xsd:date
2019-03-28
xsd:double
4.1
xsd:nonNegativeInteger
3013
xsd:date
2014-05-20
xsd:string
4.0.14
xsd:date
2019-03-28
xsd:string
4.1.22