Sep 28, 2015
Erik Poll: State machine learning: from testing to formal specifications
Finite state machines are a great specification formalism: they are intuitive and simple to understand, and can be used to describe all sorts of systems, or properties of systems, that we want to verify.
Coming up with accurate state machine models can be a lot of work. However, state machine inference provides a great technique to automatically reverse-engineer application using just black-box testing.? This can provide formal models of existing code for free, as a useful first step to rigorous specification and then verification of this code. We will show this using case studies of bank cards, internet banking tokens, and TLS implementations.