A Tutorial on Uppaal

By G. Behrmann, Alexandre David, Kim Guldstrand Larsen. International School on Formal Methods for the Design of Computer, Communication and Software Systems, 2004

1,875 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Software

View Paper: https://www.semanticscholar.org/paper/49d823ec6c0629007c406d9d58f6932719e72725

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computational Theory and Mathematics

In Software

Citations in the corpus

Uppaal SMC tutorial (2015, methodology): “Ignoring (initially) the weight annotations on locations and edges, the END locations in the three automata are easily seen to be reachable within the time intervals [6, 12], [4, 12] and [0,+∞).”
Comparing the Expressiveness of Timed Automata and Timed Extensions of Petri Nets (2008, background): “[9, 14] for an overview) demonstrate that timed automata are a suitable formalism for modelling of systems of industrial sizes and the tools have already reached a reasonable degree of maturity and efficiency.”
Challenges and Research Directions in Medical Cyber–Physical Systems (2012, methodology): “2, relies on well-known formal modeling and analysis tools, UPPAAL [10] and TIMES [6], to develop and verify the model of a system and generate code from it.”
Principles of model checking (2008, background): “Behrmann, Larsen, Petterson, and Yi and colleagues have developed the model checker Uppaal [35] since the mid-nineties.”
Contracts for System Design (2018, methodology): “Examples are the Scade Suite Design Verifier7 and Simulink Design Verifier [248], which are both based on the Prover Technology proof engine [239, 240], the products of PikeTec8 such as TPT, the tool AGATHA [55] developed at CEA/LIST and Uppaal [34] with its derivatives like Uppaal TIGA [77] and ECD”