This HTML5 document contains 117 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Namespace Prefixes

PrefixIRI
dbpedia-dehttp://de.dbpedia.org/resource/
dcthttp://purl.org/dc/terms/
yago-reshttp://yago-knowledge.org/resource/
dbohttp://dbpedia.org/ontology/
foafhttp://xmlns.com/foaf/0.1/
n27http://people.cs.aau.dk/~adavid/cora/
n12https://global.dbpedia.org/id/
yagohttp://dbpedia.org/class/yago/
n6http://www.cs.aau.dk/research/distributed-embedded-intelligent-systems/
dbthttp://dbpedia.org/resource/Template:
schemahttp://schema.org/
n18http://www.uppaal.com/
n29http://people.cs.aau.dk/~adavid/tiga/
rdfshttp://www.w3.org/2000/01/rdf-schema#
n24http://www.it.uu.se/research/group/darts/uppaal/port/
freebasehttp://rdf.freebase.com/ns/
n9http://user.it.uu.se/~hessel/CoVer/
n30http://people.cs.aau.dk/~marius/tron/
n23http://www.it.uu.se/research/group/darts/
n19http://www.uppaal.org/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
n28http://people.cs.aau.dk/~adavid/smc/
owlhttp://www.w3.org/2002/07/owl#
dbpedia-ithttp://it.dbpedia.org/resource/
wikipedia-enhttp://en.wikipedia.org/wiki/
dbphttp://dbpedia.org/property/
provhttp://www.w3.org/ns/prov#
dbchttp://dbpedia.org/resource/Category:
xsdhhttp://www.w3.org/2001/XMLSchema#
wikidatahttp://www.wikidata.org/entity/
goldhttp://purl.org/linguistics/gold/
dbrhttp://dbpedia.org/resource/
dbpedia-jahttp://ja.dbpedia.org/resource/

Statements

Subject Item
dbr:Uppaal_Model_Checker
rdf:type
schema:CreativeWork wikidata:Q386724 yago:Abstraction100002137 yago:Communication100033020 yago:Software106566077 dbo:Work yago:WrittenCommunication106349220 wikidata:Q7397 yago:CodingSystem106353757 owl:Thing yago:Writing106359877 dbo:Software yago:Code106355894
rdfs:label
Uppaal Model Checker UPPAAL Uppaal UPPAAL
rdfs:comment
Uppaal(ウパール)は、形式言語のうち、モデル検査の機能を持つシステム。時間制約付きモデルを図として記述し、検査・検証を行う。時相論理式で検査したい項目を指定する。学術向けは無償利用できるが、商用は有償。日本ではキャッツが販売代理店をしている。JAXAなど、研究開発機関での利用が進んでいる。 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. 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. 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.
foaf:name
UPPAAL
foaf:homepage
n19:
dbp:name
UPPAAL
dct:subject
dbc:Model_checkers
dbo:wikiPageID
697254
dbo:wikiPageRevisionID
900224894
dbo:wikiPageWikiLink
dbr:Uppsala_University dbr:Chinese_language dbr:Model_checking dbr:Mac_OS_X dbr:Japanese_language dbr:English_language dbc:Model_checkers dbr:Philips dbr:Timed_automaton dbr:Lego_Mindstorms dbr:Denmark dbr:Microsoft_Windows dbr:Tool dbr:Data_type dbr:Lithuanian_language dbr:Real-time_computing dbr:GUI dbr:Academic_Licenses dbr:Software_platform dbr:C++ dbr:Sweden dbr:Linux dbr:Commercial_Licenses dbr:Danish_language dbr:Java_(programming_language) dbr:Mecel dbr:Aalborg_University
dbo:wikiPageExternalLink
n6: n9: n18: n19: n23: n24: n27: n28: n29: n30:
owl:sameAs
n12:4wxGE dbpedia-ja:Uppaal dbpedia-it:UPPAAL wikidata:Q7898420 yago-res:Uppaal_Model_Checker dbpedia-de:UPPAAL freebase:m.033mmw
dbp:wikiPageUsesTemplate
dbt:Infobox_software dbt:Formalmethods-stub dbt:Release_date_and_age dbt:Reflist dbt:Start_date
dbp:developer
dbr:Aalborg_University dbr:Uppsala_University
dbp:genre
dbr:Model_checking
dbp:language
dbr:Lithuanian_language dbr:Japanese_language dbr:Chinese_language dbr:Danish_language dbr:English_language
dbp:latestReleaseDate
2014-05-20
dbp:latestReleaseVersion
4
dbp:license
dbr:Commercial_Licenses dbr:Academic_Licenses
dbp:operatingSystem
dbr:Mac_OS_X dbr:Microsoft_Windows dbr:Linux
dbp:programmingLanguage
C++ and GUI in Java
dbp:website
n18: n19:
dbo:abstract
Uppaal(ウパール)は、形式言語のうち、モデル検査の機能を持つシステム。時間制約付きモデルを図として記述し、検査・検証を行う。時相論理式で検査したい項目を指定する。学術向けは無償利用できるが、商用は有償。日本ではキャッツが販売代理店をしている。JAXAなど、研究開発機関での利用が進んでいる。 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. 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. 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.
dbp:latestPreviewDate
2019-03-28
dbp:latestPreviewVersion
4.1
gold:hypernym
dbr:Environment
prov:wasDerivedFrom
wikipedia-en:Uppaal_Model_Checker?oldid=900224894&ns=0
dbo:wikiPageLength
3013
dbo:latestReleaseDate
2014-05-20
dbo:latestReleaseVersion
4.0.14
dbo:latestPreviewDate
2019-03-28
dbo:latestPreviewVersion
4.1.22
dbo:developer
dbr:Aalborg_University dbr:Uppsala_University
dbo:genre
dbr:Model_checking
dbo:language
dbr:English_language
dbo:license
dbr:Academic_Licenses dbr:Commercial_Licenses
dbo:operatingSystem
dbr:Microsoft_Windows dbr:Mac_OS_X dbr:Linux
foaf:isPrimaryTopicOf
wikipedia-en:Uppaal_Model_Checker