This thesis investigates a method for tackling the verification of parametric systems, systems whose behaviour may depend on the value of one or more parameters. The range of allowable values for such parameters may, in general, be large or unknown. This results in a large number of instances of a system that require verification, one instance for each allowable combination of parameter values. When one or more parameters are unbounded, the family of systems that require verification becomes infinite. Computer protocols are one example of such parametric systems. They may have parameters such as the maximum sequence number or the maximum number of retransmissions. Traditional protocol verification approaches usually only analyse and verify properties of a parametric system for a small range of parameter values. It is impossible to verify in this way every concrete instance of an infinite family of systems. Also, the number of reachable states tends to increase dramatically with increasing parameter values, and thus the well known state explosion phenomenon also limits the range of parameters for which the system can be analysed. In this thesis, we concentrate on the parametric verification of the Stop-and-Wait Protocol (SWP), an elementary flow control protocol. We have used Coloured Petri Nets (CPNs) to model the SWP, operating over an in-order but lossy medium, with two unbounded parameters: the maximum sequence number; and the maximum number of retransmissions. A novel method has been used for symbolically representing the parametric reachability graph of our parametric SWP CPN model. This parametric reachability graph captures exactly the infinite family of reachability graphs resulting from the infinite family of SWP CPNs. The parametric reachability graph is represented symbolically as a set of closed-form algebraic expressions for the nodes and arcs of the reachability graph, expressed in terms of the two parameters. By analysing the reachability graphs of the SWP CPN model for small parameter values, structural regularities in the reachability graphs were identified and exploited to develop the appropriate algebraic expressions for the parametric reachability graph. These expressions can be analysed and manipulated directly, thus the properties that are verified from these expressions are verified for all instances of the system. Several properties of the SWP that are able to be verified directly from the parametric reachability graph have been identified. These include a proof of the size of the parametric reachability graph in terms of both parameters, absence of deadlocks (undesired terminal states), absence of livelocks (undesirable cycles of behaviour from which the protocol cannot escape), absence of dead transitions (actions that can never occur) and the upper bounds on the content of the underlying communication channel. These are verified from the algebraic expressions and thus hold for all parameter values. Significantly, language analysis is also carried out on the parametric SWP. The parametric reachability graph is translated into a parametric Finite State Automaton (FSA), capturing symbolically the infinite set of protocol languages (i.e. sequences of user observable events) by means of similar algebraic expressions to those of the parametric reachability graph. Standard FSA reduction techniques were applied in a symbolic fashion directly to the parametric FSA, firstly to obtain a deterministic representation of the parametric FSA, then to obtain an equivalent minimised FSA. It was found that the determinisation procedure removed the effect of the maximum number of retransmissions parameter, and the minimisation procedure removed the effect of the maximum sequence number parameter. Conformance of all instances of the SWP over both parameters to its desired service language is proved. The development of algebraic expressions to represent the infinite class of Stop-and-Wait Protocols, and the verification of properties (including language analysis) directly from these algebraic expressions, has demonstrated the potential of this method for the verification of more general parametric systems. This thesis provides a significant contribution toward the development of a general parametric verification methodology.
| Identifer | oai:union.ndltd.org:ADTP/269082 |
| Date | January 2007 |
| Creators | Gallasch, Guy Edward |
| Source Sets | Australiasian Digital Theses Program |
| Language | EN-AUS |
| Detected Language | English |
| Rights | Copyright 2007 Guy Edward Gallasch |
Page generated in 0.0171 seconds