Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2000 | 10.1016/S0167-6423(99)00017-9 | Sci. Comput. Program. |
Keywords | Field | DocType |
protocol,sscop,verication,model-checking,atm,test generation,static analysis,conformance testing,s scop,verification,sscop protocol,model checking | Programming language,Model checking,Computer science,Formal validation,Static analysis,Conformance testing,Theoretical computer science,Brute force,Interconnection,Atmosphere (unit) | Journal |
Volume | Issue | ISSN |
36 | 1 | Science of Computer Programming |
Citations | PageRank | References |
24 | 1.69 | 15 |
Authors | ||
8 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Marius Bozga | 1 | 2100 | 127.83 |
| Jean-Claude Fernandez | 2 | 24 | 1.69 |
| Lucian Ghirvu | 3 | 202 | 12.69 |
| claude jard | 4 | 1155 | 101.84 |
| Thierry Jéron | 5 | 1053 | 91.06 |
| Alain Kerbrat | 6 | 401 | 28.52 |
| Pierre Morel | 7 | 88 | 6.68 |
| Laurent Mounier | 8 | 1187 | 79.54 |