Investigating Optimal Progress Measures for Verification of the WebSocket Protocol

Abstract

The sweep-line method is a state space reduction technique for
memory-efficient on-the-fly verification of concurrent systems. The
method relies on a progress measure capturing inherent progress in the
system under verification to store only fragments of the state space in
memory at a time and thereby reduce peak memory usage. The sweep-
line method has been applied to many concurrent systems, but the
optimality of progress measures in terms of the peak number of states
stored has not been investigated. Assessing the optimality of a progress
measure is important since memory in most cases is the limiting factor
in verification using state spaces. We derive lower bounds for the peak
number states and present initial experimental results on near optimal
progress measures for verification of the IETF WebSocket protocol.