Unification & sharing in timed automata verification

Alexandre David, Gerd Behrmann, Kim Guldstrand Larsen, Wang Yi

Publikation: Bidrag til bog/antologi/rapport/konference proceedingKonferenceartikel i proceedingForskning

171 Downloads (Pure)

Abstrakt

We present the design of the model-checking engine and internal data structures for the next generation of UPPAAL. The design is based on a pipeline architecture where each stage represents one independent operation in the verification algorithms. The architecture is based on essentially one shared data structure to reduce redundant computations in state exploration, which unifies the so-called passed and waiting lists of the traditional reachability algorithm. In the implementation, instead of using standard memory management functions from general-purpose operating systems, we have developed a special-purpose storage manager to best utilize sharing in physical storage. We present experimental results supporting these design decisions. It is demonstrated that the new design and implementation improves the efficiency of the current distributed version of UPPAAL by about 60% in time and 80% in space.
OriginalsprogEngelsk
Titel10th International SPIN Workshop 2003
ForlagIEEE Computer Society Press
Publikationsdato2003
Sider225-229
StatusUdgivet - 2003
BegivenhedInternational SPIN Workshop 2003 - Portland, USA
Varighed: 5 maj 200310 maj 2003
Konferencens nummer: 10th

Konference

KonferenceInternational SPIN Workshop 2003
Nummer10th
LandUSA
ByPortland
Periode05/05/200310/05/2003
NavnLecture Notes in Computer Science
Nummer2648

    Fingerprint

Bibliografisk note

ISSN ; -

Emneord

  • Sharing
  • Passed list
  • Waiting list
  • Verification
  • Model checker

Citationsformater

David, A., Behrmann, G., Larsen, K. G., & Yi, W. (2003). Unification & sharing in timed automata verification. I 10th International SPIN Workshop 2003 (s. 225-229). IEEE Computer Society Press. Lecture Notes in Computer Science, Nr. 2648