UPPAAL model checker is one of the most important model checkers for timed systems which is widely used in both academia and industry. Suppose you have a big UPPAAL timed model and you want to use UPPAAL to check if your model satisfies certain properties. A wise approach to avoid large model checking time or more severe problems like state space explosion, is slicing the part of the model which is related to our desired properties, and only focus on that part. USlicer do that for you automatically! so you can give your timed model, and your desired properties to USlicer. USlicer gives the smaller model with respect to the properties that you are interested about. Then you can model check the resulted program using UPPAAL. USlicer is written in Python.

You can find the theory behined USlicer via following paper:

USlicer on Github: GitHub

 

Home