LOTOS based conformance testing: The theory and a tool.
Computers in a network have to obey to well-defined protocols in order to communicate properly. These protocols can be very complex and their implementation is often subject to errors. One question arises after implementing a communication protocol: does the implementation conform to its specificati...
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Others |
| Published: |
University of Ottawa (Canada)
2009
|
| Subjects: | |
| Online Access: | http://hdl.handle.net/10393/7509 http://dx.doi.org/10.20381/ruor-15379 |
| Summary: | Computers in a network have to obey to well-defined protocols in order to communicate properly. These protocols can be very complex and their implementation is often subject to errors. One question arises after implementing a communication protocol: does the implementation conform to its specification? The process of answering this question is called conformance testing. The introduction of formal description techniques, in particular LOTOS, made it possible to formalize the problem and to develop formal methods to check the conformance of implementations to their specifications. To test for conformance, tests can be derived from specifications and then applied to implementations. The CO-OP method is the basic test case generation method for LOTOS. It is used in order to generate canonical testers from specifications. The method that has been published in the literature can only deal with specifications that do not involve recursion (finite behaviours). We have generalized the CO-OP method in such a way as to remove this restriction: the only restriction we have is that the specification must have an expansion that can fit in memory. The generalized method also expands the original method to support a large subset of Full LOTOS behaviours. In most cases, testing does not prove conformance but attempts to reduce the errors in implementations. We have developed an algorithm for proving conformance in the special case of Basic LOTOS behaviours. All algorithms presented in the thesis were implemented in what we call the LOTEST tool. |
|---|