Submitted: April 2008
Abstract
While working with large and complex Uppaal models you easily get problems with the verification. The verification returns no result because the search space is too large and complex. In a lot of cases you already know which are the first steps to take to receive the desired outcome. If it would be possible to determine the first steps trough the system, the search space would shrink and the verification would be easier. For this reason the Uppaal Guider was developed in this bachelor thesis. With this program it is possible to define a determined start path and change an existing model accordingly. The thesis explains the functionality and the construction of the Uppaal Guider with examples and comments the reasons for its development.