Case Studies & Examples

Uppaal has been applied in a number of industrial case studies. Here we briefly review some of them.

More models are available at uppaal-models repository.

If you wish to contribute to this list, please email a short description of your case study.

UPPAAL

Formal Analysis of the UNISIG Safety Application Intermediate Sub-layer: modelling and analysis of the Safe Application Intermediate sub-layer of the UNISIG RBC/RBC Safe Communication Interface The contribution provides (i) rigorous complete and publicly available models of an official interface specification already in operation, (ii) identification of safety and interoperability issues in the original specification using Statistical Model Checking. Details in [pdf] [models] [doi].
Timed Automata Networks for SCADA Attacks Real-Time Mitigation: A method for detecting attacks targeting SCADA systems is proposed. By exploiting the model checking technique, we model time-series logs gathered from SCADA systems into a network of timed automata and we characterize the behaviour of a SCADA system under attack through timed temporal logic. The experimental evaluation performed on a gas distribution system confirms the effectiveness of the proposed method. Details in [ICSSA19]
Real-Time SCADA Attack Detection by means of Formal Method: We propose a method to detect attacks targeting SCADA systems. We exploit model checking, in detail we model logs from SCADA systems into a network of timed automata and, through timed temporal logic, we characterize the behaviour of a SCADA system under attack. Experiments performed on a SCADA water distribution system confirmed the effectiveness of the proposed method. Details in [WETICE19].
Modelling and Verication of Web Services Business Activity: WS-Business Activity specification defines two coordination protocols in order to ensure a consistent agreement on the outcome of long-running distributed applications. We use the model checker Uppaal to analyse the Business Agreement with Coordination Completion protocol type. The models are available here. The details are described in [RSV11].
Model-Based Framework for Schedulability Analysis: We use UPPAAL for schedulability analysis and we present a few modeling patterns. The models are available here. The details are described in a book chapter [DILS10] (bibtex).
Web Services Atomic Transaction Protocol: In this case-study, Uppaal is used to verify the consistency property of WS-AT protocol. This protocol is part of the WS-Coordination framework and describes an algorithm for reaching agreement on the outcome of a distributed transaction. The model is available here. The details are described in [RVS10].
Bang & Olufsen Audio/Video Protocol: This is an audio control protocol highly dependent on real-time. The protocol is developed by Bang & Olufsen, to transmit messages between audio/video components over a single bus, and further studied in [HSLL97]. Though it was known to be faulty, the error was not found using conventional testing methods. Using Uppaal, an error-trace is automatically produced, which revealed the error. Furthermore, a correction is suggested and automatically proved using Uppaal.
Bang & Olufsen Power Down Protocol: This is a protocol for controlling the switching between power on/off states in audio/video components described in [HLS99]. The protocol is designed by Bang & Olufsen and verified using Uppaal before the implementation work begins. The correctness of the protocol is established by automatic proofs of 15 properties derived from Bang & Olufsen’s specifications. The proofs show that additional design must be made to keep the switching time below the specified limits.
Bounded Retransmission Protocol: The protocol is proposed and studied at COST 247, International Workshop on Applied Formal Methods in System Design. It is based on the alternating bit protocol over a lossy communication channel, but allows for a bounded number of retransmissions. In [DKRT97], it is reported that a number of properties of the protocol is automatically checked with Uppaal. In particular, it is shown that the correctness of the protocol is dependent on correctly chosen time-out values.
Collision Avoidance Protocol: The protocol in [JLS96, ABL98] is implemented on top of an Ethernet-like medium such as the CSMA/CD protocol. It is to ensure an upper bound on the communication delay between the network nodes. It was designed and proved correct using Uppaal. The two main properties established show that the protocol is collision-free, and it does ensure an upper bound on the user-to-user communication delay (assuming a perfect medium).
Commercial Field Bus Protocol: This is a commercial field bus communication protocol used in various industrial environments over the world. The protocol was developed and implemented by ABB for safety-critical applications e.g. process control. This case study is one of the largest where Uppaal has been applied as reported in [DW00]. During the case study, a number of imperfections in the protocol logic and tis implementation are found and the error sources are debugged based on abstract models of the protocol; respective improvements where suggested.
Gearbox Controller: In this industrial case-study, Uppaal is applied to the design and analysis of a prototype gearbox controller for vehicles by Mecel AB [LPW98]. The gearbox controller is a component in the real-time distributed system that controls a modern car. The gear-requests from the driver are delivered via the man/machine interface over a communication network to the gearbox controller. The controller implements the actual gear change by actuating the lower level components of the system (such as the clutch, the engine and the gearbox). In the design of the controller, the symbolic simulator of Uppaal is applied to validate the system behavior. The correctness of the gear-box controller design is established by automatic proofs of 46 properties derived from requirements specified by Mecel AB.
LEGO® MINDSTROMS™ Systems - Control Program Synthesis: This work addresses the problem of synthesizing production schedules and control programs for a batch production plant model built in LEGO® MINDSTORMS™ RCX™. A timed automata model of the plant is described that faithfully reflects the level of abstraction needed to synthesize control programs. This makes the model very detailed and complicated for automatic analysis. To solve this problem a general way of adding guidance to a model by augmenting it with additional guidance variables and transition guards is presented. Applying the technique makes synthesis of control problem feasible for a plant producing as many as 60 batches. In comparison, only two batches could be scheduled without guides. The synthesized control programs have been executed in the plant. Doing this revealed some model errors. See this web site for more details.
LEGO® MINDSTROMS™ Systems - Verification of RCX™ Systems: The studied problem is that of checking properties of actual programs, rather than abstract models of programs. It is shown how Uppaal models can be automatically synthesized from RCX™ programs, written in the programming language Not Quite C, NQC. Moreover, a protocol to facilitate the distribution of NQC programs over several RCX™ bricks is developed and proved to be correct. The developed translation and protocol are applied to a distributed LEGO® system with two RCX™ bricks pushing boxes between two conveyer belts moving in opposite directions. The system is modeled and checked using Uppaal2k.
Lip Synchronization Algorithm: The algorithm is used to synchronize multiple information streams sent over a communication network, in this case, audio and video streams of a multimedia application. In [BFKLM98], the previously published algorithm specification is modeled and verified in Uppaal. Interestingly, the verification reveals some errors in the synchronize algorithm, e.g. that deadlock situations may occur before pre-described error states are reached after an error.
Multimedia Stream: [BFM98] presents the specification and verification of a multimedia stream in Uppaal. Multimedia streams are the building blocks of distributed multimedia applications. They express continuous transmission of arbitrary media types, e.g. audio or video. The stream is described in the Uppaal model and then certain real-time properties (called quality of service properties in the multimedia domain) are verified in the model-checker. Verification of throughput and end-to-end latency is particularly focused on.
Mutual Exclusion Protocol: The so-called Fischers protocol has been studied previously in many experiments. The protocol is to ensure mutual exclusion among several processes competing for a critical section using timing constraints and a shared variable. Different versions of the protocol have been verified using Uppaal, e.g. [LPW95a].
Philips Audio Protocol: The protocol is developed and implemented by Philips to exchange control information between components in audio equipment using Manchester encoding. The correctness of the encoding relies on timing delays between signals. In [LPW95b] the protocol is modeled and verified using Uppaal.
Philips Audio Protocol with Bus Collision: This is an extended variant of Philips audio control protocol with bus collision detection. It is significantly larger than the version above since several new components (and variables) are introduced, and existing components are modified to deal with bus collisions. Its correctness is originally proved by hand, and by model-checking for the first time using Uppaal in [BGKLLPW96].
TDMA Protocol Start-Up Mechanism: In [LP97], a formal verification of the start-up algorithm of a TDMA (Time Division Multiple Access) protocol is reported. It was proved using Uppaal that an ensemble of four communicating stations becomes synchronized and operational within a bounded time from an arbitrary initial state, given a clock-drift corresponding to 1/1000. Furthermore, an upper time-bound for the start-up to complete was derived.

Benchmarks

A number of older Uppaal benchmarks.