UP4ALL Inc - uppaal.com

The UPPAAL tool has been applied in a number of industrial case studies including:

ABB Field Bus Protocol: This commercial field bus communication protocol is used in various industrial environments over the world. The protocol is developed and implemented by ABB for safety-critical applications e.g. process control [DW00]. The UPPAAL tool has been used to improve the protocol logic and its implementation, based on analysis made on abstract models of the protocol; respective improvements where suggested.

Bang & Olufsen Audio/Video Protocol: 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 had some known problems, the error was not found using conventional testing methods. Using UPPAAL, an error-trace was automatically produced, which revealed the error. Furthermore, a correction was suggested and automatically proved using UPPAAL.

Bang & Olufsen Power Down Protocol: A protocol for controlling the switching between power on/off states in audio/video components described in [HLS99]. The protocol was designed by Bang & Olufsen and verified using Uppaal before the implementation work began. The correctness of the protocol was established by automatic proofs of 15 properties derived from Bang & Olufsen's specifications. The proofs showed that additional design must be made to keep the switching time below the specified limits.

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.

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).

Gearbox Controller: UPPAAL is applied to design and analyse 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^TM 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^TM RCX^TM. 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.

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.