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.
| Attributes | Values |
|---|
| rdf:type
| |
| rdfs:label
| - UPPAAL (de)
- UPPAAL (it)
- Uppaal (ja)
- Uppaal Model Checker (en)
|
| rdfs:comment
| - Uppaal（ウパール）は、形式言語のうち、モデル検査の機能を持つシステム。時間制約付きモデルを図として記述し、検査・検証を行う。時相論理式で検査したい項目を指定する。学術向けは無償利用できるが、商用は有償。日本ではキャッツが販売代理店をしている。JAXAなど、研究開発機関での利用が進んでいる。 (ja)
- 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. (de)
- 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. (it)
- 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. (en)
|
| foaf:name
| |
| foaf:homepage
| |
| name
| |
| dcterms:subject
| |
| Wikipage page ID
| |
| Wikipage revision ID
| |
| Link from a Wikipage to another Wikipage
| |
| Link from a Wikipage to an external page
| |
| sameAs
| |
| dbp:wikiPageUsesTemplate
| |
| developer
| |
| genre
| |
| language
| |
| latest release date
| |
| latest release version
| |
| license
| |
| operating system
| |
| programming language
| |
| website
| |
| has abstract
| - 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. (de)
- 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. (en)
- Uppaal（ウパール）は、形式言語のうち、モデル検査の機能を持つシステム。時間制約付きモデルを図として記述し、検査・検証を行う。時相論理式で検査したい項目を指定する。学術向けは無償利用できるが、商用は有償。日本ではキャッツが販売代理店をしている。JAXAなど、研究開発機関での利用が進んでいる。 (ja)
- 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. (it)
|
| latest preview date
| |
| latest preview version
| |
![[RDF Data]](/fct/images/sw-rdf-blue.png)
![[cxml]](/fct/images/cxml_doc.png)
![[csv]](/fct/images/csv_doc.png)
![[text]](/fct/images/ntriples_doc.png)
![[turtle]](/fct/images/n3turtle_doc.png)
![[ld+json]](/fct/images/jsonld_doc.png)
![[rdf+json]](/fct/images/json_doc.png)
![[rdf+xml]](/fct/images/xml_doc.png)
![[atom+xml]](/fct/images/atom_doc.png)
![[html]](/fct/images/html_doc.png)