[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] Concerning the verification of a protocol in PVS



Hello:

    I am a PVS beginner and recently I am trying to verify a "conflict handling mechanism/protocol" by PVS. The formal specification of this protocol bears a couple of challenges for me. I know there are many PVS experts in this mail list, thus I will be very thankful if I can get some help from you. The system where the protocol is applied is presented as follows:

    The target system is a component-based system, which is composed of a set of hierarchically organized components (here we focus on software components). The figure in the attachment illustrates a typical component-based system. Component a is at the top level and it is composed of b and c. b is composed of d, e and f… A component is called "composite component" if it is composed of other components, e.g. a and b. A component is called "primitive component" if it cannot be further decomposed, e.g. g and h. A primitive component is usually directly implemented by code. Apparently the componenthierarchy has a tree structure and components at adjacent levels have parent-children relationship. For instance, b is the parent of d, e, f, which in turn are the children/subcomponents of b. This is not a binary tree because a composite component can have arbitrary number of children. The system conforms to CBSE (Component-Based Software Engineering), which has component reuse as a key feature. Since a component is independently developed without knowing the context in which it will be reused, it will be unaware of the other parts of the system when it is reused. For instance, in this example, b knows the information of its children d, e, f, but does not know the information of other components at further lower nested levels. Component b may also know that it has a parent, but it does not know who is its parent. However, a knows the information of both b and c.

    This protocol is used to handle the concurrent signal transmission between parents and children. First let's list different types of signals and some special components.

 

Signals:

1. Request (R): sent from a component to its parent

2. Instruction (I): sent from a parent to one or more of its children (as a result of receiving R)

3. Denial (D): sent from a parent to one particular child as a result of receiving R

4. OK: sent from a component to its parent as a result of receiving I

 

Rules for transmitting these signals will be explained later in the protocol description.

 

Definition:

1. Source (S): a component which can actively send an R to its parent

2. Top: The component at the top level, e.g. Component a in this example

3. Decision Maker (DM): a composite component which sends an I or D to its children after processing an R

 

S and DM will be further explained in the description of this protocol partitioned into the following rules:

 

1.    Any component can be an S, spontaneously sending an R to its parent (if it is not Top) and expecting a response, either an I or an D. If Top is an S, it can actively send an I to its children. An S will not send another R or I before it receives a response of its previous R or I. In this example, we define Component d as S1 and Component l as S2.

2.    Each primitive S component x has one R queue (FIFO queue). When it sends an R to its parent, this R is also put in its R queue. A primitive non-S component has no R queue. This R is removed from the R queue when a corresponding I or D is received (see Rule 6).

3.    Each composite component (either S ornon-S) y has two queues: R queue and I queue (FIFO queue). R queue is the same as a primitive S component. The difference is that it has R queue even if it is not an S itself because it may receive an R from a child. We assume each R is associated with a component ID so that y knows which child has sent this R to it before. When y receives an R from a child, this R will be added in its R queue. I queue is used to store any incoming I from the parent.

4.    Any composite component x sending an I to one or more of its children expects a corresponding OK acknowledgment. Component x is not allowed to send OK to its parent until it has collected all expected OK from its children. If x is Top, there is no need to send OK. (Rule 6 explains when and how I is sent)

5.    Each component has two states: stable state (M, initial state) and intermediate state (N). A component is in state N within the interval [t1, t2], where t1 is the moment when it sends an I to its children, and t2 is the moment when it receives all expected OK. Otherwise, it is instate M.

6.    In state M, a composite component xactively and periodically checks its I and R queues while I queue has a higher priority. I queue will be first checked. If there is any pending I in the I queue, it will be processed by x and removed from the I queue. As theprocessing result, x may send another I to none, one or more of its children. Besides, each I should be able to tell which R it is associated with. If this I is associated with the first element in the R queue of x, the first R in the R queue should also be removed. Otherwise, the R queue is unaffected. If I queue is empty, R queue will be checked. If R queue is not empty, the first pending R will be processed. As the processing result, x may 1)send an I (this I is associated with the R being processed) to one or more of its children (the child which sent this R to x before must be included); 2)send D to the child which sent this R to x before; 3)forward this R to the parent of x, i.e. by sending another R (including the ID of x) to its parent. In the first two cases, this R will be removed from the R queue and x is considered to be the DM (Decision Maker). In the last case, this R stays in the R queue and the DM should be one ancestor of x in the component hierarchy. These three cases should be modeled as random decisions in PVS and only one of them is taken each time. For each R, there must be a corresponding DM, which could be any ancestor of the S component that initiates this R in the component hierarchy. If x happens to be Top, it will only have the first two choices (the last choice requires that x has a parent).

7.    In state N, any component x is not allowed to send any signal. But it can receive a signal (we conjecture thatthis signal can only be I, R or OK, but not D in this condition). Any incoming I or R will be added in the corresponding I or R queues of x.

8.    We enforce a minimum interval between two consecutive Rs or Is (the activeinitiation of I implies Top is an S) from the same S. This interval should be long enough so that the system will not be always occupied with processing Rs from the same S while the R from another S is never processed.

9.    After receiving an I from the parent or sending an I to the children, a component may keep or change its role, i.e. from an S to a non-S or viceversa. Therefore, the set of all Ss of a system can vary from time to time. This is decided by the system designer. However, I and R queues do not change together with a component’s role.

 

As can be seen, this protocol is not trivial in that many concurrent activities could take place. As a PVS beginner, I really do not know what to start with. I have identified several challenges which must be overcome:

1.    Presenting the component hierarchy. The hierarchy has a tree structure. The depth level of the tree can be arbitrary and a composite component can have arbitrary number of children. Besides, any component can be an S, yet possibly not always. I used to verify systems by model checking. However, this type of system will easily give rise to state explosion. This is the main reason why I resort to PVS. I don’t know if there is any built-in tree data structure in PVS and I cannot find any PVS example using the tree structure. Or we may manually build the tree but I have no idea of achieving this yet.

2.    Modeling I and R queues. I guess we can use the “sequence” data structure in the PVS prelude, however, I haven’t found any example using “sequence”. It would be much easier to use it by following a related but simple example.

3.    Specifying non-deterministic choices. For instance, a component may make a decision out of three possible choices at random according to Rule 6.

4.    Specifying the timing. According to Rule 8, we enforce a minimum interval to prevent too frequent signal transmission and starvation of some signals. Also, we may also need to indicate time while formulating some properties. For instance, a key property is: an S will eventually receive either an I or D from its parent after it sends an R to its parent.

 

I sincerely hope that this problem can arise your interest and I can get some valuable suggestions from you. If anything about the protocol is unclear, please feel free to point it out. Thank you in advance!

Best regards,

Yin Hang


----------------------------------------

Yin Hang                             

Ph.D. Student

Email: young.hang.yin@xxxxxx

phone: +4621101619

Mälardalen University, MRTC

Västerås, Sweden

Attachment: ComponentHierarchy.jpg
Description: ComponentHierarchy.jpg