|
Using the formal Communication Fintie State Machine (CFSM)
model, a communication protocol consists of several
communicating entities which can be represented in some CFSMs.
Since communication techniques are improved day by day and the
required services are changed recently, e.g., the services for
multimedia networking, existing protocols in computer networks
may need to be changed accordingly. Instead of specifying
protocols from scratch, existing protocols may be incrementally
respecified by adding or deleting some functions to meet the
new requirement. To ensure that the modified protocols are free
from logical errors, e.g, deadlock error, unspecified reception
error, and channel overflow error, protocol vertification still
needs to be invoked. Therefore, the key issue of incremental
protocol specification based on existing protocols is to ensure
that the modification will not result in logical errors. This
thesis proposes a vertification method, which is called the
reverse protocol verification, to detect logical errors for
incremental protocol specification. By analyzing the properties
of deadlock error, unspecified reception error, and channel
overflow error, some candidate erroneous global states are
generated. Then, each candidate global state is checked whether
there is a path, i.e, a global state sequence, connects to the
original initial global state. If there is a path, then the
candidate global state is really an erroneous global state and
the incrementally specified protocol does have some logical
errors. Otherwise, if there is no candidate global state or
none of the candidate global states has a path, then the
incrementally specified protocol is error free.
|