Scaling up Uppaal Automatic Verification of Real-Time Systems Using Compositionality and Abstraction
Henrik Ejersbo Jensen, Kim G. Larsen, Arne Skou · 2000
To combat the state-explosion problem in automatic verification, we present a method for scaling up the real-time verification tool Uppaal by complementing it with methods for abstraction and compositionality. We identify a notion of timed ready simulation which we show is a sound condition for preservation of safety properties between realtime systems, and in addition is a precongruence with respect to parallel composition. Thus, it supports both abstraction and compositionality. We furthermore present a method for automatically testing for the existence of a timed ready simulation between real-time systems using the Uppaal tool.