440
S. Wimmer and J. von Mutius
Variant
Model
Size
1
2a
2b
2c
2d
2e
FDDI
8
0.21 0.21 1.72 69.53 3.65 3.43
FDDI broadcast 8
0.00 48.94 48.94 48.94 1.06 1.06
Fischer
5 22.03 22.03 22.72 43.06 30.40 30.40
CSMA/CD
5 26.06 41.54 43.84 81.16 58.94 47.54
6 24.86 41.91 44.02 88.35 63.24 47.02
Mode
Pacemaker
1 16.07 25.00 30.80 58.04 29.02 29.02
2 24.00 26.38 30.37 58.68 35.87 35.22
3 12.96 17.62 19.23 46.92 25.30 25.01
4 13.82 20.02 23.60 41.48 26.16 24.71
5 17.14 22.48 25.46 39.69 28.18 26.88
Average
15.71 26.61 29.07 57.58 30.18 27.03
Table 2: Certificate compression factors (given in %).
6 Conclusion and Future Work
We have presented a verified certifier of unreachability certificates for a timed
automata. The certificates are ought to be produced by an unverified model
checker. Experimentation shows that verified certificate checking in isolation is up
to an order of magnitude faster than what was previously possible with a verified
model checker [31]. The performance of a tandem of an unverified model checker
and the verified certifier could be improved by replacing the certificate-producing
part with a highly optimized tool, possibly opening room to use some of the more
powerful certificate compression techniques we suggested above. As we pointed
out above, there appears to be further room for improvement on the certificate
compression algorithms as well.
Moreover, more sophisticated tools also employ more powerful abstraction
techniques, for which our proposed certification technique is still suitable—to a
large extent without requiring additional verification effort. An exception is the
implicit abstraction technique studied by Herbreteau et al. [14] as it does not
compute abstractions of zones explicitly but rather checks subsumptions of the
form Z ⊆ α(Z
) implicitly, meaning that one would have to prove correctness of
the subsumption check to validate certificates produced by such a model checking
process.
Finally, we intend to extend this work to certification of emptiness of timed
B¨ uchi automata in the future, using the idea of subsumption graphs [13] and
relying on an unverified model checker implementation for timed B¨ uchi automata
to produce the certificates [13,18].
S. Wimmer and J. von Mutius
Variant
Model
Size
1
2a
2b
2c
2d
2e
FDDI
8
0.21 0.21 1.72 69.53 3.65 3.43
FDDI broadcast 8
0.00 48.94 48.94 48.94 1.06 1.06
Fischer
5 22.03 22.03 22.72 43.06 30.40 30.40
CSMA/CD
5 26.06 41.54 43.84 81.16 58.94 47.54
6 24.86 41.91 44.02 88.35 63.24 47.02
Mode
Pacemaker
1 16.07 25.00 30.80 58.04 29.02 29.02
2 24.00 26.38 30.37 58.68 35.87 35.22
3 12.96 17.62 19.23 46.92 25.30 25.01
4 13.82 20.02 23.60 41.48 26.16 24.71
5 17.14 22.48 25.46 39.69 28.18 26.88
Average
15.71 26.61 29.07 57.58 30.18 27.03
Table 2: Certificate compression factors (given in %).
6 Conclusion and Future Work
We have presented a verified certifier of unreachability certificates for a timed
automata. The certificates are ought to be produced by an unverified model
checker. Experimentation shows that verified certificate checking in isolation is up
to an order of magnitude faster than what was previously possible with a verified
model checker [31]. The performance of a tandem of an unverified model checker
and the verified certifier could be improved by replacing the certificate-producing
part with a highly optimized tool, possibly opening room to use some of the more
powerful certificate compression techniques we suggested above. As we pointed
out above, there appears to be further room for improvement on the certificate
compression algorithms as well.
Moreover, more sophisticated tools also employ more powerful abstraction
techniques, for which our proposed certification technique is still suitable—to a
large extent without requiring additional verification effort. An exception is the
implicit abstraction technique studied by Herbreteau et al. [14] as it does not
compute abstractions of zones explicitly but rather checks subsumptions of the
form Z ⊆ α(Z
) implicitly, meaning that one would have to prove correctness of
the subsumption check to validate certificates produced by such a model checking
process.
Finally, we intend to extend this work to certification of emptiness of timed
B¨ uchi automata in the future, using the idea of subsumption graphs [13] and
relying on an unverified model checker implementation for timed B¨ uchi automata
to produce the certificates [13,18].