@article{Bengtsson_Larsen_Larsson_Pettersson_Yi_1996, title={UPPAAL—a Tool Suite for Automatic Verification of Real–Time Systems}, volume={3}, url={https://tidsskrift.dk/brics/article/view/18769}, DOI={10.7146/brics.v3i58.18769}, abstractNote={Uppaal is a tool suite for automatic verification of safety and<br />bounded liveness properties of real-time systems modeled as networks of<br />timed automata. It includes: a graphical interface that supports graphical<br />and textual representations of networks of timed automata, and automatic<br />transformation from graphical representations to textual format,<br />a compiler that transforms a certain class of linear hybrid systems to<br />networks of timed automata, and a model-checker which is implemented<br />based on constraint-solving techniques. Uppaal also supports diagnostic<br />model-checking providing diagnostic information in case verification of a<br />particular real-time systems fails.<br />The current version of Uppaal is available on the World Wide Web via<br />the Uppaal home page http://www.docs.uu.se/docs/rtmv/uppaal.}, number={58}, journal={BRICS Report Series}, author={Bengtsson, Johan and Larsen, Kim G. and Larsson, Fredrik and Pettersson, Paul and Yi, Wang}, year={1996}, month={Jun.} }