Efficient Verification Of Timed Systems Using Backward Reachability Analysis

Jesper B. Møller

Publikation: Bog / Antologi / Rapport / Ph.D.-afhandlingRapportForskning

Abstract

In this paper we demonstrate that symbolic verification of real-time systems based on backward reachability analysis is generally more efficient than verification based on forward reachability analysis. Symbolic verification of real-time systems consists of computing the least fixpoint of a functional that given a set of states phi returns the states that are reachable from phi (forward reachability), or that can reach phi (backward reachability). The key observation is that the symbolic operations in the fixpoint computation can be simplified substantially when performing backward reachability analysis. In particular, we show that resetting clocks and making discrete state changes can be performed as substitutions instead of existential quantifications over reals and Booleans, respectively. Experimentally we find that backward reachability analysis is more efficient than forward reachability analysis.
OriginalsprogEngelsk
UdgivelsesstedCopenhagen
ForlagIT-Universitetet i København
UdgaveTR-2002-11
Antal sider13
ISBN (Elektronisk)87-7949-015-8
StatusUdgivet - feb. 2002
Udgivet eksterntJa
NavnIT University Technical Report Series
NummerTR-2002-11
ISSN1600-6100

Fingeraftryk

Dyk ned i forskningsemnerne om 'Efficient Verification Of Timed Systems Using Backward Reachability Analysis'. Sammen danner de et unikt fingeraftryk.

Citationsformater