Simplifying Fixpoint Computations in Verification of Real-Time Systems

Jesper B. Møller

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

Abstract

Symbolic verification of real-time systems consists of computing the least fixpoint of a functional which given a set of states $\phi$ returns the states that are reachable from $\phi$ (in forward reachability), or that can reach $\phi$ (in backward reachability). This paper presents two techniques for simplifying the fixpoint computation: First, I demonstrate that in backwards reachability, clock resets and discrete state changes can be performed as substitutions instead of existential quantifications over reals and Booleans, respectively. Second, I introduce a local-time model for real-time systems which allows clocks to advance asynchronously, thus resulting in an over-approximation of the least fixpoint, but which in some cases is sufficient for verifying a temporal property.
OriginalsprogEngelsk
UdgivelsesstedCopenhagen
ForlagIT-Universitetet i København
UdgaveTR-2002-15
Antal sider13
ISBN (Elektronisk)87-7949-020-4
StatusUdgivet - apr. 2002
Udgivet eksterntJa
NavnIT University Technical Report Series
NummerTR-2002-15
ISSN1600-6100

Fingeraftryk

Dyk ned i forskningsemnerne om 'Simplifying Fixpoint Computations in Verification of Real-Time Systems'. Sammen danner de et unikt fingeraftryk.

Citationsformater