This is a tutorial paper on the tool Uppaal. Its goal is to be a short introduction on the flavor of
timed automata implemented in the tool, to present its interface, and to explain how to use …

About a decade after the initial proposal to use model checkers for the generation of test
cases we take a look at the results in this field of research. Model checkers are formal …

This tutorial paper surveys the main features of Uppaal SMC, a model checking approach in
Uppaal family that allows us to reason on networks of complex real-timed systems with a …

This paper describes a major new release of the PRISM probabilistic model checker,
adding, in particular, quantitative verification of (priced) probabilistic timed automata. These …

Cyber-physical systems (CPSs) are the next generation of engineered systems in which
computing, communication, and control technologies are tightly integrated. Research on …

Abstract Model checking is an automatic technique for verifying finite-state reactive systems,
such as sequential circuit designs and communication protocols. Specifications are …

We consider the following clustering problem: we have a complete graph on n vertices
(items), where each edge (u, v) is labeled either+ or− depending on whether u and v have …

Nature discovered feedback long ago. It created feedback mechanisms and exploited them
at all levels, that are central to homeostasis and life. As a technology, control dates back at …

The majority of work carried out in the formal methods community throughout the last three
decades has (for good reasons) been devoted to special languages designed to make it …

This chapter is to provide a tutorial and pointers to results and related work on timed
automata with a focus on semantical and algorithmic aspects of verification tools. We …