|
FPTA Model Checker XYZ Research Group,
Key Lab of Computer Science |
| ¡¡ Finite precision timed automaton(FPTA) is a timed automaton with integer clock values. The feature that differentiates FPTA from other discrete timed or digital timed models is that it can distinguish the ordering of clock changing, by the introduction of order, an auxiliary integer variable for every clock, which explicitly records the ordering among fractional parts of clock values. The first version of the prototype tool for reachability analysis of FPTAs was developed in 2003. It unfolds all the states in the state space without any symbolic technology. So it can only verify small examples. Examples, including using shared variables, synchronizing transitions cases, have been examined to verify their properties, and compared with other tools to check whether the results are correct. The second version of the prototype uses one symbolic state to record a sequence of states generated from time delays. However, from the experiment results, this symbolic method needs refining. The current version of the prototype organizes the sequences of states generated from time delay according to their relations. And the experiment results prove that its performance is much better than the former versions. But there are still lots of work to be done to refine the tool. The prototype keeps on updating. Here you can download the executable files and some examples. FPTA is available for the Microsoft Windows platforms.
The executable files consist of two parts, one is the compiler of source descriptions on the models, and the other is a GUI to provide the environment to input or open the descriptions and the properties. Please extract the compressed files into the same folder. The examples include both source descriptions and compiled results. Users can open the .obj files and checking the model directly. ¡¡ |
Welcome any questions and comments.