Search

In this paper, we present a method for automatic verificationof real-time control programs running on LEGO RCX bricks using the verification tool UPPAAL. The controlprograms, consisting of a number of tasks running concurrently,are automatically translated into the timed automatamodel of UPPAAL. The fixed scheduling algorithmused by the LEGO RCX processor is modeled in UPPAAL,and supply of similar (sufficient) timed automatamodels for the environment allows analysis of the overallreal-time system using the tools of UPPAAL. To illustrateour techniques we have constructed, modeled and verifieda machine for sorting LEGO bricks by color.

A rather new approach towards compositional verification of concurrent systems is the quotient technique, where components are gradually removed from the concurrent system while transforming the specification accordingly. When the intermediate specifications can be kept small using heuristics for minimization, the state explosion problemis avoided and there are already promising experimental results for systems with an interleaving semantics, including real-time systems. This paper extends the quotienting approach to deal with a synchronous framework in the shape of state/event systems. A state/event system is a concurrent system with a set of interdependent components operating synchronously according to stimuli (input events) provided by an environment while producing output events in return for the environment. A compositional modal logic M suitable for expressing general safety and liveness properties subsystems is introduced. A quotient construction for building components from a state/event system into the specification is presented and heuristics for minimizing formulae are proposed. The techniques are demonstrated on an example. The correctness of the techniques are justified by proofs in an appendix.

In this paper, we apply acompositional proof technique to an automaticverification of the correctness ofFischer's mutual exclusion protocol. Itis demonstrated that the technique mayavoid the state-explosion problem. Ourcompositional technique has recently beenimplemented in a tool, CMC, which givesexperimental evidence that the size ofthe verification effort required of the techniqueonly grows polynomially in thesize of the number of processes in theprotocol. In particular, CMC verifies theprotocol for 50 processes within 172.3seconds and using only 32MB main memory.In contrast all existing verificationtools for timed systems will suffer fromthe state-explosion problem, and no toolhas to our knowledge succeeded in verifyingthe protocol for more than 11 processes.