The Verus Language: Representing Time Efficiently with BDDs

There 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 timecritical 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. ...

• Type: Conference
• Year: 1997
• Where: ARTS
• Authors: Sérgio Vale Aguiar Campos, Edmund M. Clarke
• Keywords: ARTS 1997, Complex Systems, Distributed And Parallel Computing, Formal Methods, Special Constructs