Formal modeling and analysis of a narrow bandwidth protocol for establishing and terminating connections
The paper presents a formal modeling and analysis of a protocol for narrow bandwidth channels of service connection establishment and termination. The protocol is characteri zed by state traces and formally verified by a theorem proving system PVS. Relevant prope rties are specified and verified in terms of inductive principles. The effectiveness of the proposed method is evidenced by the elaborate analysis which unveils a subtle bug in the initial protoco limplementation. The approach is scalable for an arbitrary number of agents. (C) 2009 Elsevier Ltd. All rights reserved.
narrow bandwidth theorem proving pvs connection establishment protocol