Verification and test generation for the SSCOP protocol

Many formal tools are now efficient enough to deal with small-to-medium size systems. Working with larger systems requires not so much to improve these tools, but to use them in combination, applying one tool for what it is most efficient for, and using its results to improve the applicability of the other tools. This paper presents such a combination, illustrated on an industrial protocol, large enough to break any brute force approach. Two research teams allied their forces with a software engineering tools maker in order to analyse, verify and generate automatically tests for this protocol, by the extension and the interconnection of their various tools. The results obtained give some hints on a methodology for the formal validation of large systems.