Slicing for UPPAAL

Student thesis: Master Thesis and HD Thesis

  • Uffe Sørensen
  • Claus Rørbæk Thrane
4. term, Computer Science, Master (Master Programme)
The focus of this thesis is to introduce slicing for Uppaal. Slicing is a technique based on static analysis used to reduce the syntactic size of models or applications. In this thesis, we show how slicing may be used to construct reachability preserving reductions of Uppaal models possibly improving the performance of the tool. Using automated slicing in Uppaal will eliminate the need for users to manually optimize models for faster verification of a certain property. Moreover, it allows less experienced users of Uppaal, which unknowingly may design models, containing unnecessary large amounts of data, to verify properties which Uppaal otherwise would have been unable to check.
Publication dateJun 2007
ID: 61073108