The Verus language: representing time efficiently with BDDs

AbstractThere have been significant advances on formal methods to verify complex systems recently. Nevertheless, these methods have not yet been accepted as a realistic alternative to the verification of industrial systems. One reason for this is that formal methods are still difficult to apply efficiently. Another reason is that current verification algorithms are still not efficient enough to handle many complex systems. This work addresses the problem by presenting a language designed especially to simplify writing time-critical programs. It is an imperative language with a syntax similar to C. Special constructs are provided to allow the straightforward expression of timing properties. The familiar syntax makes it easier for non-experts to use the tool. The special constructs make it possible to model the timing characteristics of the system naturally and accurately. A symbolic representation using BDDs, model checking and quantitative algorithms are used to check system timing properties. The efficiency of the representation allows complex realistic systems to be verified