Addressing Current Limitations of Real-time Model-checking

Model checkers are tools which can automatically verify that a system behaves as intended. Because this is done on a model of a system, design flaws are identified before the system is actually built, thus saving time, money, and even loss of lives (e.g. systems that control the navigation of airplanes). Here we focus on real-time model-checking, which deals with systems where timing constraints are important.A (real-time) model-checker accepts a model represented as a network of timed automata. Timed automata are a graph-like notation where nodes represent states in the system behaviour, and arcs between nodes represents actions. Both the time when actions can be performed, and the amount of time the system may remain in a given state, can be constrained. The second input to model-checkers is a logic formula, describing the correctness property we wish to check (e.g, that a certain undesired event will never occur). The logic is usually known as the requirements logic.Model-checking is one of the triumphs of theoretical computer science research, with a large number of successful applications in the commercial sector. This is because model-checkers can now automatically verify properties which, in the past, required experts to develop complex proofs by hand. Among real-time model-checkers, Uppaal is the most extensively applied. The success of Uppaal in bridging the gap between academic research and industrial application is impressive. However, the approach still has a number of significant limitations:1. Timelocks. These are degenerate states in which time is unable to pass and cannot, in the general case, be detected. Timelocks arise because of the way in which the passage of time is modelled in timed automata semantics. Of course, physical systems cannot stop time. However, the verification of properties by model-checkers is (for reasons that I will not address here) only meaningful for timelock-free models. If a model contains a timelock, then the user cannot have complete confidence in the verification results. For example, Uppaal may report that a bad event never occurs, unaware that the event may indeed occur, but cannot be detected because the model stops time before this happens. Dangerously, this undetected bad event may still be present when the system is built.2. Expressiveness of Requirements Logic. Uppaal is very efficient. But to achieve this, the designers had to limit the kind of properties which can be written (i.e they had to restrict the requirements logic). As a result, many properties that one would like to verify cannot be checked with Uppaal, or are difficult to express (and so it is easier to make mistakes when trying to capture the meaning of a given property).The proposed research will address these limitations and thereby significantly improve the applicability of real-time model-checking in general, and Uppaal, in particular. This will be done as follows.1. Building from existing related work on the subject I will develop techniques and tools to prevent or detect timelocks in timed automata specifications (these are based on the structure of the timed automata).2. I will integrate research on choppy logics (more expressive than Uppaal's logic) with test automata approaches (a different way to express properties, which Uppaal can handle efficiently) to enlarge the class of properties that Uppaal can model-check, without compromising its performance. 3. I will undertake a set of demanding case studies to evaluate our Uppaal extensions (e.g. control systems, communication protocols, sensor networks, etc.).4. Finally, I will feed the results of our research into fields of computing for which symbolic real-time model checking is critical.