The Computer Journal · 1994 · 49 citations · 0 references
ComputingComputer ScienceComputer SystemsDistributed SystemsFormal MethodsParallel ComputingConcurrency VerificationData-flow AnalysisDeductive VerificationProcess AlgebraProtocol AnalysisProtocol VerificationCorrectness ProofsInvariant-based VerificationModel Checking For ConcurrencyModel ParallelismProcess Algebra VerificationSliding Window ProtocolsSliding Window Verification
We model a one-bit sliding window protocol and prove that its external behaviour is a bi-directional buffer of capacity 2. The proof is given in µCRL, which is a process algebra extended with data. Due to the abundant parallelism in this protocol, the behaviour is quite complicated. The complexity has been mastered by explicitly identifying invariants and foci of cones in the protocol. Both concepts seem promising as tools for the verification of larger and more complex protocols.