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.

Property Value
dbo: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 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)
dbo:category
dbo:developer
dbo:latestReleaseDate
  • 2010-09-27 (xsd:date)
dbo:latestReleaseVersion
  • 4.0.13
dbo:license
dbo:operatingSystem
dbo:wikiPageExternalLink
dbo:wikiPageID
  • 8612713 (xsd:integer)
dbo:wikiPageRevisionID
  • 145961900 (xsd:integer)
prop-de:autor
  • Bourke, Timothy and Sowmya, Arcot
  • Larsen, Kim G. and Pettersson, Paul and Yi, Wang
  • Braspenning, N. C. W. M. and Bortnik, E. M. and van de Mortel-Fronczak, J. M. and Rooda, J. E.
  • Xing, Jiansheng and Theelen, Bart D. and Langerak, Rom and Van De Pol, Jaco and Tretmans, Jan and Voeten, J. P. M.
prop-de:band
  • 13 (xsd:integer)
  • 59 (xsd:integer)
prop-de:deutsch
  • nein
prop-de:doi
  • 101016 (xsd:integer)
  • 101145 (xsd:integer)
prop-de:herausgeber
  • Springer-Verlag
  • ACM
  • Elsevier Science Publishers B. V.
prop-de:issn
  • 166 (xsd:integer)
prop-de:jahr
  • 1997 (xsd:integer)
  • 2008 (xsd:integer)
  • 2010 (xsd:integer)
  • 2013 (xsd:integer)
prop-de:monat
  • dec
  • jan
prop-de:nummer
  • 1 (xsd:integer)
  • 3 (xsd:integer)
prop-de:reihe
  • 1 (xsd:integer)
  • ISoLA'10
prop-de:sammelwerk
  • ACM Trans. Embed. Comput. Syst.
  • Comput. Ind.
  • International Journal on Software Tools for Technology Transfer
  • Proceedings of the 4th International Conference on Leveraging Applications of Formal Methods, Verification, and Validation - Volume Part II
prop-de:zugriff
  • 2015-08-27 (xsd:date)
dc:description
  • Model Checker
dct:subject
rdf:type
rdfs:comment
  • 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 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)
rdfs:label
  • UPPAAL (de)
  • UPPAAL (de)
owl:sameAs
prov:wasDerivedFrom
foaf:homepage
foaf:isPrimaryTopicOf
foaf:name
  • UPPAAL (de)
  • UPPAAL (de)
foaf:page
is foaf:primaryTopic of