Related publications: [DTLS20]
The benchmark contains Mealy machine models generated for DTLS 1.2 servers as part of work presented at USENIX. The models are between 10-66 states in size, except for JSSE which are significantly larger.
Below is a heavily pruned version of an over 100 state model obtained for Java 12. In red are the problematic transitions, transitions on paths to the teal state which should not have been allowed. The teal state is the so-called handshake-completed state, a state in which the DTLS session has been established.
