The Verus language: Representing time efficiently with BDDs
type: Item
instance of: scholarly article
title: The Verus language: Representing time efficiently with BDDs
zbMATH Open document ID: 0954.68098
DOI: 10.1016/S0304-3975(00)00090-6
author: Sérgio Campos
author: Edmund Clarke
published in: Theoretical Computer Science
publication date: 2000-12-12T00:00:00Z
review text: 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 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.
Mathematics Subject Classification ID: 68Q60
zbMATH DE Number: 1542355
zbMATH Keywords: symbolic model checking
zbMATH Keywords: timed systems
zbMATH Keywords: BDDs
zbMATH Keywords: verus
describes a project that uses: Esterel
MaRDI profile type: Publication
cites work: Q4038702
cites work: The Esterel synchronous programming language: Design, semantics, implementation
cites work: A brief history of Timed CSP
cites work: Q4037378
cites work: Symbolic model checking for real-time systems
cites work: TIC: a tImed calculus
full work available at URL: s0304-3975(00)00090-6
OpenAlex ID: W2650981837
description: scientific article; zbMATH DE number 1542355