| Summary: | The verification of a "sup" property based on a clock value does not terminate | ||
|---|---|---|---|
| Product: | UPPAAL | Reporter: | Hang Yin <young.hang.yin> |
| Component: | Engine | Assignee: | Alexandre David <adavid> |
| Status: | NEW --- | ||
| Severity: | normal | ||
| Priority: | P2 | ||
| Version: | 4.1.3 | ||
| Hardware: | Macintosh | ||
| OS: | Mac OS | ||
| Architecture: | |||
| Attachments: | The xml and q files of the model | ||
This is a pipe-and-filter system consisting of two components a and b. The system has one input and output. A data source generates new data to the system periodically. The system uses a counter to monitor the number of data being processed inside. The component connection is very simple. Data flow is like: Data source-->system-->a-->b-->system-->output. A threshold is defined to limit the maximal possible number of data simultaneously being processed in the system. When the threshold is reached, the data source will be turned off until the number of data in the system is smaller than the threshold again. Both a and b have input buffers. When they are not processing any data, the first data in the buffer will be processed immediately. a and b are also one group with atomic execution. This is also a multi-mode system which can switch mode. A Mode Switch Request (MSR) could arrive at any time from a Mode Switch Triggering Source (MSTS). When the system receives the MSR, the data source is turned off and no more input data will enter the system until all the data currently being processed by the system are flushed away. The purpose of the second and third property is to find out the worst-case latency introduced by the atomic execution of this group made of a and b, when a MSR arrives. Created attachment 254 [details]
The xml and q files of the model
|
By using traditional UPPAAL modeling and verifying techniques (the second property in the property list), it can be found that the maximal clock value in state "Waiting" of "MSTS" is 12. But the property "sup{MSTS.Waiting}: MSTS.x" does not terminate. It is expected that the same value 12 should be obtained from its verification result. The "sup" property works fine in some other states of other templates, but the reason why it does not terminate in x.N is unknown.