当前位置:首页 >> >>

Software design, specification, and verification Lessons learned from the Rether case study

Software Design, Speci cation, and Veri cation: Lessons Learned from the Rether Case Study?
Xiaoqun Du, Kevin T. McDonnell, Evangelos Nanos, Y.S. Ramakrishna, Scott A. Smolka
Department of Computer Science SUNY at Stony Brook Stony Brook, NY 11794{4400, USA

Abstract. Rether is a software-based real-time ethernet protocol developed at SUNY Stony Brook. The purpose of this protocol is to provide guaranteed bandwidth and deterministic, periodic network access to multimedia applications over commodity ethernet hardware. It has been implemented in the FreeBSD 2.1.0 operating system, and is now being used to support the Stony Brook Video Server (SBVS), a low-cost, ethernet LAN-based server providing real-time delivery of video to end-users from the server's disk subsystem. Using local model checking, as provided by the Concurrency Factory speci cation and veri cation environment, we showed (for a particular network con guration) that Rether indeed makes good on its bandwidth guarantees to real-time nodes without exposing non-real-time nodes to the possibility of starvation. In the course of specifying and verifying Rether, we identi ed an alternative design of the protocol that warranted further study due to potential e ciency gains. Again using model checking, we showed that this alternative design also possesses the properties of interest.

1 Introduction
Rether is a software-based real-time ethernet protocol developed at SUNY Stony
Brook by Tzi-cker Chiueh and Chitra Venkatramani CV95]. The purpose of this protocol is to provide guaranteed bandwidth and deterministic, periodic network access to multimedia applications over commodity ethernet hardware. It has been implemented in the FreeBSD 2.1.0 operating system, and is now being used to support the Stony Brook Video Server (SBVS), a low-cost, ethernet LAN-based server providing real-time delivery of video to end-users from the server's disk subsystem. The MAC layer of ethernet uses the CSMA/CD protocol, which provides nondeterministic channel access to the nodes on the network. This form of access is unsuitable for real-time multimedia applications such as video conferencing. Rether is a datalink layer protocol that runs on top of CSMA/CD and requires no modi cation to the ethernet hardware. It accommodates real-time applications by using a token to regulate the transmission of packets in the network. At any time, only the node that holds the token is allowed to transmit. Therefore, nodes are provided deterministic and contention-free channel access.

Research supported in part by NSF grants CCR-9505562 and CCR-9705998, and AFOSR grants F49620-95-1-0508 and F49620-96-1-0087.

In discussions with Rether's developers, it became clear that they would welcome some kind of formal assurance that their protocol does indeed deliver guaranteed bandwidth to real-time nodes without running the risk of starving non-real-time nodes. To this end, we set out to formally verify these properties of Rether using the Concurrency Factory speci cation and veri cation environment CLSS96]. The primary features of the Factory are its graphical user interface for speci cation and simulation of hierarchical networks of communicating state machines; its VPL textual speci cation language for describing protocols involving complex data structures and value passing; and its suite of analysis routines for verifying properties of speci cations. One of the main analysis routines supported by the Factory is model checking CE81, QS82, CES86], a veri cation technique for determining whether a system speci cation possesses a property expressed as a temporal logic formula. Model checking has enjoyed wide success in verifying, or nding design errors in, real-life systems. An interesting account of a number of these success stories can be found in CW96]. A distinguishing aspect of the Factory's model checker is its use of local model checking , a technique aimed at combating state explosion by performing state space search in a need-driven fashion. To carry out the proposed veri cation of Rether, we encoded the protocol in the Factory's VPL speci cation language and submitted this speci cation to the local model checker. A number of temporal logic properties were model checked, including the two mentioned above, and in all cases the speci cation was shown to possess the property of interest. In the course of using the Factory to verify Rether, it occurred to us that an alternative design of the protocol might also be worth investigating. Rether, as it is currently implemented in FreeBSD, services the real-time nodes rst during any given token rotation cycle; the period of a cycle is determined by the frequency of the real-time data transmissions. After servicing the real-time nodes, non-realtime requests are serviced until the cycle bandwidth is exhausted. We refer to this method as the real-time rst (RTF) node servicing policy. In our alternative policy, nodes are serviced in sequential order (SQO) by their node ids. One of the bene ts of the SQO policy is that, under certain reasonable assumptions, it incurs less tokenpassing overhead than RTF. This is because a node wishing to transmit real-time and non-real-time data within one cycle may do so in SQO during the same visit of the token. RTF, on the other hand, would require the token to make a second visit to the node in question in order for it to transmit its non-real-time data. SQO also requires less information to be stored in the token: in RTF, the token must maintain a bit vector indicating which nodes are in real-time mode. In order to verify that the Rether developers could safely use our new policy, we submitted an SQO-based VPL speci cation of Rether to the Factory's local model checker. As in the original RTF-based protocol, the model checker revealed that all properties of interest were satis ed. Interestingly, our model checking experiments show that the size of the Rether state space goes down by a factor of four in moving from RTF to SQO. In light of the above, the following lessons were learned from our Rether case study: 1. By requiring one to write an abstract and formally rigorous speci cation of a

system, speci cation and veri cation can have a positive (and perhaps unexpected) in uence on software design. In our case, this was the discovery of the SQO node servicing policy. We believe this phenomenon is primarily one of being able to see the forest through the trees once an abstract speci cation is in hand. This view is consistent with that of Parnas in Par96], who wrote on the topic of software jewels: These] Programs were not just written; they had been planned, often in some pseudocode or a language other than the actual programming language. 2. Alternative software designs can be shown \equivalent" through veri cation. 3. An alternative software design may lead to a smaller state space, thereby facilitating model checking and other forms of veri cation. 4. Interesting properties of real-time protocols can be veri ed without the use of real-time formalisms, such as timed automata AD94] or real-time logic Mok91]. For our Rether case study, we abstracted real time into \time slots" and, in this context, it su ced to use an untimed value-passing language (VPL) along with a non-real-time temporal logic (the modal mu-calculus Koz83]). Our use of the time-slots abstraction to model the real-time behavior of the Rether protocol is discussed in greater detail in Section 5. The structure of the rest of the paper is as follows. Sections 2 and 3 provide overviews of the Concurrency Factory and Rether protocol, respectively. Our alternative software design is the subject of Section 4. Section 5 describes how we speci ed the protocol in VPL, both for RTF and SQO. Our model checking results are presented in Section 6, and conclusions and directions for future work in Section 7.

2 The Concurrency Factory
The Concurrency Factory CLSS96] is an integrated toolset for the speci cation, veri cation, and implementation of concurrent and distributed real-time systems such as communication protocols and process control systems. The main features of the Factory are: a graphical user interface that allows the non-expert to design and simulate concurrent systems using GCCS, a graphical process algebra; a textual user interface for VPL; a suite of veri cation routines that currently includes a local model checker with partial-order reduction RS97] for the modal mu-calculus, a very expressive temporal logic, and a local model checker for a real-time extension of the modal mu-calculus SS95]; and a graphical compiler that transforms GCCS and VPL speci cations into executable Facile TLK96] code. We brie y describe here the components of the Factory that are most germane to our veri cation of the Rether protocol: VPL and the local model checker for the modal mu-calculus. VPL is well suited for specifying concurrent systems with non-trivial control structure and data structures, and which involve value passing (as opposed to pure synchronization). VPL-supported data structures include integers of limited size and arrays and records composed of such integers. Structural equivalence of data types is employed, i.e. two integer types are considered the same

if their sizes are equal and two records are equivalent when they have elds of the same type appearing in the same order. A system speci cation in VPL is a tree-like hierarchy of subsystems. A subsystem is either a network or a process . A network consists of a collection of subsystems running in parallel and communicating with each other through typed channels. Processes are at the leaves of the hierarchy. Each subsystem, be it a process or a network, consists of a header, local declaration and body. The header speci es a unique name for the subsystem and a list of \formal channels" (by analogy with formal parameters of procedures in programming languages). The names of the formal channels of a subsystem can be used in the body of the subsystem and represent events visible to an external observer. Declarations local to a network include speci cations of the subsystems of the network and channels for communication between subsystems, hidden from the outside world. The body of a network is a parallel composition of its subsystems. A subsystem declared within a network can be used arbitrarily many times; each time a new copy of the subsystem is instantiated with actual channels substituted for the formal ones. Actual channels must match the formal ones introduced in the header and must be declared either as local channels or formal channels of the network immediately containing the subsystem. Declarations local to a process consist of variable and procedure declarations. Procedure bodies, like process bodies, are sequences of statements. Simple statements of VPL are assignments of arithmetic or boolean expressions to variables, and input/output operations on channels. Complex statements include sequential composition, if-then-else, while-do, and nondeterministic choice in the form of the select statement. VPL programs can be veri ed using LMC, the Concurrency Factory's local model checker for the propositional modal mu-calculus. LMC rst produces a graph representation of the logical formula under consideration and then computes the product of this graph with the labeled transition system (guaranteed to be nitestate) underlying the VPL program. This \product graph" is constructed on-the- y: each product graph node has an associated boolean value (representing the value of a subformula in an LTS state) and the value of a node is computed based on the values of its successors. Values of the terminal nodes in the product graph can be decided immediately based on the node itself. Nodes are never constructed unless their values are needed to determine the value of a previously constructed node. To further reduce the size of the product graph, LMC avoids interleaving process transitions whenever the order of interleaving cannot a ect the truth of a logical formula. Intuitively, this is achieved by enlarging the granularity of process steps so as to avoid redundant interleavings. LMC is also equipped with a diagnostic facility that allows the user to request that the contents of the depth- rst search stack be displayed whenever a certain \signi cant event" occurs|for instance, when the search rst encounters a state at which a logical variable is determined to be either true or false. This technique can be used to great e ect, for instance, to discover execution paths leading to deadlocked states, or to livelock cycles.

3 The Rether Protocol
Rether is a contention-free token bus protocol for the datalink level, designed to run on top of a CSMA/CD physical layer. A network running the protocol normally operates in CSMA/CD mode, transparently switching to Rether mode when one or more nodes generate requests for real-time (RT) connections. An initialization protocol is used to coordinate the switch to Rether mode. Once in Rether mode, a token is used to control access to the medium. That is, a node can transmit data on the network only when it has the token. The token circulates the network in cycles, each of which is called a token rotation cycle . The period of a cycle, the token cycle time , is a con gurable parameter determined by the frequency of real-time data transmissions. For instance, TCT (as this parameter is called) can be set to 33.3 ms for video applications, which typically transmit data at the rate of 30 frames per second. In each token cycle, all nodes that have successfully made a bandwidth reservation (the so-called \admitted nodes") can send out RT data in accordance with their reservations. In the time remaining in the cycle, nodes are permitted to send out non-real-time (NRT) data. To be fair to NRT transmission requests, part of each cycle, Tnrt , is set aside for NRT tra c. An RT application is admitted into the system by the protocol only if there is su cient bandwidth in the cycle. That is, suppose this application requests a reservation for an RT transmission of duration THT RT (where THT stands for \token holding time"). Then this request is granted only if the following inequality holds: !


where RT set is the set of admitted RT nodes, and THT RT is the token holding time of the ith RT node. It is precisely this policy that enables the protocol to guarantee cycle bandwidth to RT applications. Admitted RT nodes are serviced rst in a cycle, and we refer to this policy as RTF. A newly admitted RT application adds its node id to RT set, which is stored in the token as a bit vector. A node releasing RT bandwidth removes its id from RT set before forwarding the token to the next node. The network reverts back to CSMA/CD mode when the last RT node releases its bandwidth. The token also carries a \residual time" counter, which records the amount of time remaining in a cycle. At the start of a cycle this eld is initialized to TCT . Following a data transmission by the token-holding node, the residual time counter is decremented by that node's token holding time before the token is passed to the next node. The admission policy ensures that at least Tnrt time remains in each cycle for NRT tra c. NRT transmissions are scheduled in a round-robin fashion to prevent the possibility of starvation. For this purpose, the token carries a eld containing the id of the last node that failed to transmit its NRT data in a given cycle because of insu cient residual time. To illustrate the behavior of the protocol, and the RTF node servicing policy, consider the example network depicted in Figure 1. RT set contains 1, 3, and 5 and these nodes are serviced rst during each token rotation cycle. Assuming that

i2RT set

THT RT i + THT RT new + Tnrt



Nodes with only NRT data



Nodes with RT and possibly NRT data

RT traffic 1 3 5

NRT traffic 1, 2, 3 1 3 5 4, 5, 1

First Token Cycle

Second Token Cycle

Fig. 1. A Sample Network Con guration.
each cycle can accommodate three NRT transmissions (in addition to the three guaranteed RT transmissions), and that each node has NRT data to transmit, it takes two successive cycles for the NRT transmissions to be serviced in round-robin fashion. In particular, the following sequences of node transmissions are possible in successive cycles: 1{3{5{1{2{3 1{3{5{4{5{1

4 SQO: An Alternative Node Servicing Policy
As mentioned in the Introduction, in the process of specifying and verifying Rether, we identi ed an alternative design of the protocol that warranted investigation because of potential e ciency gains. In this version, nodes are serviced in sequential order by their node ids, a policy we refer to as SQO. In order to ensure periodic access to the token by RT nodes, the node with the smallest node id number is the rst to receive the token in each cycle. Upon receiving the token, a node will transmit its RT data if it has previously been admitted by the protocol as an RT node. It will also, during the same token visit, transmit a xed amount of NRT data if: (1) it has NRT data to transmit, and (2) the \next" pointer, which is stored in the token and used to implement round-robin scheduling, indicates that su cient NRT bandwidth remains in the current cycle to accommodate the node's transmission. The next-pointer is incremented when its value is i and node i has just completed an NRT transmission. Similarly, an NRT node (i.e. a node with only NRT data to transmit) transmits its data only if there is su cient bandwidth. Otherwise, it simply passes the token to its neighbor. Note that, unlike RTF, there is no need in the SQO policy to store RT set in the token.

To further illustrate the SQO strategy, consider once again the network of Figure 1. The following sequences of node transmissions are possible in successive cycles: (1-1) { 2 { (3-3) { (4) { 5 (1-1) { (2) { 3 { 4 { (5-5) where a sequence item of the form (i-i) means that node i transmits both RT and NRT data during the same token visit. Also, an item of the form (i) means that i is an NRT node that transmits no data but rather just passes the token along to its neighbor. At the beginning of the rst sequence, the next-pointer is set to 1, which means that the NRT data transmissions of nodes 1, 2, and 3 can be accommodated during this cycle. The value of the next-pointer will be 4 at the beginning of the second sequence, allowing nodes 4, 5, and 1 to transmit NRT data. Comparing these sequences to the corresponding ones for RTF given above, we see that the token visits a total of ve nodes per cycle in SQO, and six nodes per cycle in RTF. In general, SQO will incur less token-passing overhead than RTF when the total number of per-cycle data transmissions (call this m) exceeds the number of nodes on the network (call this n). Moreover, the reduction in overhead increase linearly in m ? n. If m < n, SQO could potentially require more token passing than RTF, depending on the relative ordering of RT and NRT nodes. In practice, though, the conditions favorable to SQO can be expected to occur frequently, and correspond to the situation where the network is not saturated by too many applications with RT demands.

5 VPL Speci cation of Rether
In this section, we describe how we speci ed the Rether protocol in VPL for both the original RTF version, and our alternative SQO version. The interested reader can nd the VPL source code listings at http://cs.sunysb.edu/~sas/rether.html. The key to the speci cations, and subsequent model checking, is our abstraction of time into \time slots." That is, each token cycle is divided into a xed number of time slots, and each RT and NRT transmission consumes one time slot. Since the properties we wish to verify (admitted RT nodes receive their guaranteed cycle bandwidth and NRT transmissions are not starved) do not depend on the exact value of the token holding times, our time slot abstraction is su cient for this purpose. Both versions of the protocol are speci ed in VPL as a network of N+2 processes: Node_0, : : :, Node_N-1, Token, and Bandwidth. The Node_i processes capture the behavior of the various nodes in the network, Token represents the Rether token, and Bandwidth is the process that nodes interact with to reserve or release cycle bandwidth. A separate process is set aside for the token in order to localize the token-passing logic deployed by the protocol. Modeling the token in this fashion decreases the size of the speci cation's state space. Figure 2 depicts the network topology of the speci cation. In particular, it indicates the names of the channels that processes use to communicate with one another and with the outside world. To simplify the gure, only Node_0 is depicted;


nrt_0 reserve_0 release reserve





ok not_ok



grant no_grant



Fig. 2. Network topology of the speci cation.
the other nodes are connected to Token, Bandwidth, and the outside world in a similar fashion. The connections to the outside world are for model-checking purposes. That is, actions over these channels will appear in the various modal mu-calculus formulas to be model checked. Each such action represents a pure synchronization and the signi cance of these actions is as follows:
start: indicates the beginning of a token cycle cycle: indicates the end of a token cycle reserve_i: Node_i successfully makes a bandwidth rt_i: Node_i performs an RT transmission nrt_i: Node_i performs an NRT transmission


Since the contents of the transmitted data is irrelevant to the correct operation of the protocol, it su ces to use the signals rt_i and nrt_i in their place. Process Bandwidth is perhaps the simplest of the processes in the speci cation, and we start with it. It essentially behaves as a counting semaphore whose value should not exceed RTSlots, where RTSlots is the total number of time slots available in a token cycle for RT data transmissions. RTSlots is less then the total number of time slots (Slots) in a cycle since some slots are reserved for NRT tra c. An RT node requests a bandwidth reservation via the signal reserve. The request is granted if a time slot is available; i.e., if RT_count < RTSlots where RT_count is a local variable that keeps track of the number of RT nodes in the system. When an RT node is ready to release its reserved bandwidth, it signals Bandwidth with release. It is ok for the node to release its bandwidth and become an NRT node as long as the system contains at least one RT node at all times. This is to ensure that the protocol remains in Rether mode: the protocol reverts back to

CSMA/CD mode when all RT connections terminate, and we do not model this mode of the protocol. Bandwidth also writes RT_count to channel RTC_chan when Token wants to read the number of RT nodes in the system. Process Bandwidth is common to the RTF and SQO speci cations. The di erence in these versions of the protocol lies in the behavior of the other processes in the network. We consider rst the behavior of these processes for the RTF version. The Token process determines the order in which the token visits the nodes in the network. It is also responsible for starting and ending the token rotation cycle and updating the information in the token at the beginning of each cycle. To perform these duties, it maintains a local data structure tok_value with the following elds: a bit-vector node ] used to encode RT set; an integer NRT_count indicating the number of time slots available for NRT data transmissions in the current cycle (NRT_count is decremented each time an NRT data transmission occurs); an integer next, which points to the next node with NRT data to be serviced in round-robin fashion; and a boolean variable serving_rt, which indicates whether RT tra c or NRT tra c is currently being serviced. Token starts a cycle by outputting the signal start to the outside world. It then passes the token to each of the nodes in RT set in order by their node ids. Token passes the token to Node_i by writing the token data structure onto channel visit i]; when Node_i is nished with the token it sends it back to Token over the same channel. After nishing with the RT nodes, Token circulates the token among the nodes in the system until all remaining time slots are consumed. At this point, Token terminates the cycle by outputting the signal cycle and setting NRT_count to Slots ? RT_count (recall that RT_count is maintained by the bandwidth process). It then begins a new cycle. In the RTF version of Rether, process Node_i rst receives the token from process Token into the local variable local_tok. It then checks local_tok.serving_rt to determine if it should call procedure RT_action or NRT_action. (In the RTF model, only an RT node can get the token with serving_rt true.) Procedure RT_action simulates an RT data transmission by emitting signal rt_i, and then nondeterministically chooses to release its bandwidth. If its request to release bandwidth is successful, the node is deleted from RT set and local_tok.node i] is updated accordingly. Node_i executes procedure NRT_action when it receives the token and local_tok.serving_rt is false. The following conditions are guaranteed to hold at this point: Node_i is being pointed to by local_tok.next and the value of local_tok.NRT_count is greater than zero. Therefore, it simulates an NRT transmission by emitting signal nrt_i, decrementing local_tok.NRT_count, and incrementing local_tok.next. NRT_action then checks local_tok.node i] to see if it is an RT node; if not, it nondeterministically chooses to issue a request for bandwidth reservation. If granted, local_tok.node i] is set to true, making Node_i an RT node, and signal reserve_i is emitted to the outside world, indicating that Node_i has successfully made a bandwidth reservation. Upon completion of NRT_action, Node_i outputs local.tok to Token. Process Token is somewhat simpler in the SQO-based speci cation of the protocol than in the RTF-based one. It has simpler token-passing logic|the token is passed from one node to another in sequential order by their node ids|and

the token carries less information in it since it no longer stores RT set. In particular, tok_value has the following four elds: RT_count, NRT_count, next, and NRT_enabled. RT_count and NRT_count are the residual number of time slots for RT and NRT data transmissions, respectively, and next and NRT_enabled are used to implement round-robin scheduling of NRT transmissions. NRT_enabled is set to true by Token if the NRT data transmission of the next node to receive the token can be accommodated during the current cycle. This is the case if the following (somewhat complicated looking) condition is met:
NRT_count > 0 & ( next = index | ( index <next & total_NRT > N - next + index ) )

Here index is the id of the next node to receive the token, total_NRT is the total number of time slots available in the current cycle for NRT transmissions, and N is the total number of nodes in the network. The reader is referred to the discussion of the SQO policy in Section 4 for the intuition underlying this logic. Process Node_i in the SQO case has a local variable mode indicating whether or not the node is an RT node. Similar to the RTF case, once Node_i receives the token, it calls RT_action or NRT_action depending on the value of mode. In RT_action, it emits signal rt_i and decrements local_tok.RT_count to simulate an RT data transmission. If local_tok.NRT_enabled is true, it also emits signal nrt_i and decrements local_tok.NRT_count. Moreover, it increments local_tok.next if local_tok.next = i. As in the RTF case, it can then nondeterministically choose to release its bandwidth reservation; if successful, it switches to NRT_mode. The SQO version of NRT_action also checks local_tok.NRT_enabled to decide if it can perform an NRT data transmission. If it can, it behaves as does RT_action in this case, after which it may nondeterministically choose to request a bandwidth reservation. If this request is granted, Node_i switches to RT_mode.

6 Model Checking the Rether Protocol
In this section, we summarize the results we obtained applying the Concurrency Factory's local model checker to our VPL speci cations of the Rether protocol. To ensure that we are model checking a nite-state system, we xed the following parameters of the speci cation at compilation time: the number of nodes in the system is chosen to be 4, i.e. the system contains Node_0 up to Node_3; the total number of time slots in each token rotation cycle (Slots) is 3; and one slot per cycle is reserved for NRT data transmission. Consequently, during each cycle there are either two RT transmissions plus one NRT transmission, or two NRT transmissions plus one RT transmission. Initially Node_0 is designated as an RT node and is pointed to by next. The remaining nodes are initially NRT nodes. We model checked both versions of the protocol (RTF and SQO) against 14 formulas of the modal mu-calculus, expressing di erent properties of the system. The syntax of the modal mu calculus makes use of propositional constants tt and , logical variables X , Y and Z , standard logical connectives _ and ^, dual modal operators h?i and ?], and dual xed point operators (least xed point) and (greatest xed point). A formula of the form h?i is true of a state s if it is possible


X:( ?]X ^ h?itt) X:( ?]X ^ start] Y:(h?itt ^ start] ^ ?cycle]Y )) X:( ?]X ^ reserve0 ] Y:( ?cycle]Y ^ rt0 ] ^ cycle] Z:(h?itt ^ ?rt0 ]Z ^ cycle] ))) X:( ?]X ^ reserve1 ] Y:( ?cycle]Y ^ rt1 ] ^ cycle] Z:(h?itt ^ ?rt1 ]Z ^ cycle] ))) X:( ?]X ^ reserve2 ] Y:( ?cycle]Y ^ rt2 ] ^ cycle] Z:(h?itt ^ ?rt2 ]Z ^ cycle] ))) X:( ?]X ^ reserve3 ] Y:( ?cycle]Y ^ rt3 ] ^ cycle] Z:(h?itt ^ ?rt3 ]Z ^ cycle] ))) X:( ?]X ^ start] Y:( ?fnrt0 ; cycleg]Y ^ cycle] Z:( ?nrt0 ]Z ^ h?itt))) X:( ?]X ^ start] Y:( ?fnrt1 ; cycleg]Y ^ cycle] Z:( ?nrt1 ]Z ^ h?itt))) X:( ?]X ^ start] Y:( ?fnrt2 ; cycleg]Y ^ cycle] Z:( ?nrt2 ]Z ^ h?itt))) X:( ?]X ^ start] Y:( ?fnrt3 ; cycleg]Y ^ cycle] Z:( ?nrt3 ]Z ^ h?itt))) X:( ?]X ^ start] Y:( cycle] ^ h?itt ^ ?SRT ]Y )) X:( ?]X ^ start] Y:( cycle] ^ h?itt ^ ?SNRT ]Y )) X0 :( ?]X0 ^ start] X1 :( ?S ]X1 ^ cycle] ^ S ] X2 :( ?S ]X2 ^ cycle] ^ S ] X3 :( ?S ]X3 ^ cycle] ^ S ] X4 :( ?cycle]X4 ^ S ] ))))) X:( ?]X ^ SNRT ] Y:(h?itt ^ ?cycle]Y ^ SRT ] ))
i i


Table 1. Formulas we model checked. S is the set frt ; nrt j0 frt j0 i 3g and SNRT is the set fnrt j0 i 3g.
i i


3g, SRT is the set

for s to perform an action and reach a state where holds. Dually, ?] is true of s if necessarily after s performs an action it reaches a state where holds. In place of `?' (any action) a speci c action a or an expression of the form `?a' (meaning any action except a) can appear inside the modal operators. Fixed point formulas are of the form X : (X ) or X : (X ). Intuitively, formulas capture eventuality properties and formulas capture invariant properties. The modal mu-calculus formulas we model checked are listed in Table 1. Their meaning can be understood as follows: { DLF: Deadlock freedom. { CC: Cycle completion. This formula states that each token rotation cycle must be completed. It requires that whenever the beginning of a cycle is seen ( start ]), then eventually the end of the cycle must also be seen by observing the signal cycle , and that there cannot be another start before the cycle is observed. { RT0 - RT3: Bandwidth guarantee for RT nodes. These formulas state that whenever Node_i successfully makes a bandwidth reservation during a token rotation cycle ( reserve i ]... cycle ]), then during the immediate following cycle (i.e. before a second cycle signal is seen), Node_i will transmit RT data ( rt i ]). Also no RT data transmission for this node is allowed during the cycle in which it made the reservation (the node is not yet an RT node in that cycle).

{ NS0 - NS3: No Starvation for NRT tra c. If during a particular cycle, a Node_i does not transmit any NRT data (i.e. no nrt i between start and cycle ), then eventually an nrt i signal will be observed, meaning that Node_i eventually { RTT: At least one RT data transmission in each cycle. Once a start is seen, at least one signal from the set frti j0 i 3g must be observed before the cycle { NRT: At least one NRT data transmission in each cycle. Once a start is seen, at least one signal from the set fnrti j0 i 3g must be observed before the { T3T: A total of three data transmissions in each cycle. Once a start is seen, there must be exactly three signals from the set frti ; nrti j0 i 3g before the { RTF: RT- rst property. This formula states that in each cycle, if an NRT data

transmits some NRT data.


cycle signal.

cycle signal.

transmission is observed, no more RT data transmissions can be seen before the end of the cycle. This implies that all RT data transmissions must precede any NRT data transmissions in each cycle.

Our model checking results for the RTF and SQO models are summarized in Tables 2 and 3, respectively. All data is obtained from a Sun4m Sparc machine with 65MB RAM and 520MB swap space. All the formulas turn out to be true for the RTF model, as intended. For the SQO model, all formulas except RTF are true, again as intended.
Formula Result States (K) Transitions (K) Memory (MB) Time (min) DLF True 49.2 53.4 11.0 80.6 CC True 93.9 100.2 16.2 125.3 RT0 True 40.5 42.9 7.9 42.6 RT1 True 42.7 45.7 8.2 45.5 RT2 True 43.9 47.0 8.4 47.4 RT3 True 43.4 45.8 8.2 45.7 NS0 True 100.2 107.0 17.2 129.8 NS1 True 100.7 107.6 17.3 129.2 NS2 True 100.8 107.7 17.3 128.9 NS3 True 101.7 108.9 17.5 131.4 RTT True 44.7 47.2 8.4 47.8 NRT True 79.9 85.6 14.0 100.2 T3T True 82.1 86.6 13.0 82.7 RTF True 52.3 55.4 9.7 59.0

Table 2. Model cheking results for the RTF model.
Within each model, for the formulas RT0 through RT3, there are some small di erences in their state count. This is due to the fact that our system is not strictly symmetric, since Node_0 starts out as an RT node, while the others start out as

Formula Result States (K) Transitions (K) Memory (MB) Time (min) DLF True 12.0 13.7 3.0 19.9 CC True 22.6 25.1 4.2 25.4 RT0 True 10.9 12.0 2.3 10.7 RT1 True 11.3 12.7 2.4 12.4 RT2 True 11.5 12.9 2.4 12.1 RT3 True 10.4 11.5 2.2 10.3 NS0 True 19.4 21.4 3.6 22.8 NS1 True 21.8 24.1 4.0 26.2 NS2 True 21.9 24.3 4.0 25.7 NS3 True 25.0 27.8 4.5 31.0 RTT True 13.7 15.2 2.8 15.1 NRT True 14.7 16.5 3.0 17.3 T3T True 19.8 21.7 3.4 18.8 RTF False 1.8 1.8 0.9 2.6

Table 3. Model checking results for the SQO model.
NRT nodes. Also, the token visits the nodes in a speci c order in each cycle. These reasons also explain the minor variation among the data obtained for formulas NS0 through NS3. Owing to its simpler token-passing logic, the SQO model has a smaller state space than the RTF model: there is roughly a factor of four di erence between the number of the states explored by the Concurrency Factory's local model checker. Consequently, the number of transitions, the memory usage, and the execution time are all down by roughly a factor of four in the SQO model.

7 Conclusion
We used the Concurrency Factory's local model checker to verify a number of key properties of the Rether real-time ethernet protocol. In the course of specifying and verifying Rether, we identi ed an alternative design of the protocol that warranted further study because of potential e ciency gains. Model checking was used to show that this alternative design also possessed the properties of interest. As for future work, it would be interesting to implement the SQO node servicing policy in the FreeBSD kernel, so that its performance could be compared to the original protocol. It would also be interesting to observe its relative impact on the quality of service (e.g. jitter) in video applications. Another research direction is to prove Rether correct for an arbitrary number of nodes and cycle time slots. This will require induction-based techniques, e.g. MK95], symbolic techniques for parameterized systems, e.g. KMM+ 97], or more general theorem-proving techniques, e.g. RSS95].

R. Alur and D. Dill. The theory of timed automata. TCS, 126(2), 1994. E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. In D. Kozen, editor, Proceedings of the Workshop on Logic of Programs, Yorktown Heights, volume 131 of Lecture Notes in Computer Science, pages 52{71. Springer-Verlag, 1981. CES86] E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic veri cation of nitestate concurrent systems using temporal logic speci cations. ACM TOPLAS, 8(2), 1986. CLSS96] R. Cleaveland, P. M. Lewis, S. A. Smolka, and O. Sokolsky. The Concurrency Factory: A development environment for concurrent systems. In R. Alur and T. A. Henzinger, editors, Computer Aided Veri cation (CAV '96), volume 1102 of Lecture Notes in Computer Science, pages 398{401, New Brunswick, New Jersey, July 1996. Springer-Verlag. CV95] T. Chiueh and C. Venkatramani. The design, implementation and evaluation of a software-based real-time ethernet protocol. In Proceedings of ACM SIGCOMM '95, pages 27{37, 1995. CW96] E. M. Clarke and J. M. Wing. Formal methods: State of the art and future directions. ACM Computing Surveys, 28(4), December 1996. KMM+ 97] Y. Kesten, O. Maler, M. Marcus, A. Pnueli, and E. Shahar. Symbolic model checking with rich assertional languages. In Proceedings of the 9th International Conference on Computer-Aided Veri cation, Haifa, Israel, July 1997. Springer-Verlag. Koz83] D. Kozen. Results on the propositional -calculus. Theoretical Computer Science, 27:333{354, 1983. MK95] K. L. McMillan and R. Kurshan. A structural induction theorem for processes. Information and Computation, 117:1{11, 1995. Mok91] A. K. Mok. Toward mechanization of real-time system design. In A. van Tilborg and G. Koob, editors, Foundations of Real-Time Computing: Formal Speci cations and Methods, pages 1{38. Kluwer Academic Publishers, 1991. Par96] D. L. Parnas. Why software jewels are rare. IEEE Computer, 29(2):57{61, February 1996. QS82] J. P. Queille and J. Sifakis. Speci cation and veri cation of concurrent systems in Cesar. In Proceedings of the International Symposium in Programming, volume 137 of Lecture Notes in Computer Science, Berlin, 1982. Springer-Verlag. RS97] Y. S. Ramakrishna and S. A. Smolka. Partial-order reduction in the weak modal mu-calculus. In Proceedings of the Eighth International Conference on Concurrency Theory (CONCUR '97). Springer-Verlag, July 1997. RSS95] S. Rajan, N. Shankar, and M. K. Srivas. An integration of model checking with automated proof checking. In P. Wolper, editor, Computer Aided Veri cation (CAV '95), volume 939 of Lecture Notes in Computer Science, pages 84{97, Liege, Belgium, July 1995. Springer-Verlag. SS95] O. Sokolsky and S. A. Smolka. Local model checking for real-time systems. In Proceedings of the 7th International Conference on Computer-Aided Veri cation. American Mathematical Society, 1995. TLK96] B. Thomsen, L. Leth, and T.-M. Kuo. A Facile tutorial. In Proceedings of the Seventh International Conference on Concurrency Theory (CONCUR '96), Vol. 1119 of Lecture Notes in Computer Science, pages 278{298. SpringerVerlag, 1996. A This article was processed using the L TEX macro package with LLNCS style AD94] CE81]



All rights reserved Powered by 甜梦文库 9512.net

copyright ©right 2010-2021。