A Java toolkit for the design and the automatic checking of server architectures
Gautier Loyauté, Rémi Forax, Gilles Roussel · 2007
This paper presents Saburo, a Java toolkit that generates, from a single Java specification, Java Internet server implementations, together with their formal model that can be automatically checked using the model checker SPIN. This approach ensures the coherence between the Internet server behavior and the static verifications applied on its formal model. Moreover, the use of the Java language as a unique input specification should help the dissemination of formal verification techniques.