|Summary:||wrong verification results when many template instances are used|
|Product:||UPPAAL||Reporter:||Marius Mikučionis <marius>|
|Component:||Engine||Assignee:||Gerd Behrmann <behrmann>|
dining cryptographers model
queries for dining cryptographers protocol
Description Marius Mikučionis 2007-11-19 13:39:17 CET
I have a model of dining cryptographers. Currently it is hopeless that verification could scale with many cryptographers in the system (due to unexploited ring symmetry), however UPPAAL claims to verify the problem with 1000 cryptographers in a few seconds, that is something I did not expect. The closer look revealed serious correctness problems, like some trivial states are not reachable when many processes are instantiated, but they are reached when only a handful is used. My guess is that there is some kind of buffer overflow problem either with transition filter (many broadcast synchronization combinations) or template instantiation. The UPPAAL version from the trunk suffers the same problems, and in addition it reports 0 time and 0 memory used, which hints that there are some stability issues.
Comment 1 Marius Mikučionis 2007-11-19 13:39:50 CET
Created attachment 200 [details] dining cryptographers model
Comment 2 Marius Mikučionis 2007-11-19 13:40:23 CET
Created attachment 201 [details] queries for dining cryptographers protocol
Comment 3 Alexandre David 2007-11-29 18:13:36 CET
The bug was caused by an overflow. This is detected in rev. 3350.