Browsing by Author "Miller, Raymond E."
Now showing 1 - 9 of 9
Results Per Page
Sort Options
Item Analyzing the Point Coordination Function of the IEEE 802.11 WLAN Protocol using a Systems of Communicating Machines Specification(2002-05-22) Youssef, Moustafa A.; Miller, Raymond E.A model for the specification and analysis of communication protocols called Systems of Communicating Machines is used to specify an IEEE 802.11 Point Coordination Function protocol, and to analyze it for safety and certain restricted liveness properties. The model uses a combination of finite state machines and variables in the specification of each machine, and the communication between machines is accomplished through shared variables. Enabling predicates and actions are associated with each transition; the enabling predicates determine when a transition may be taken, and the actions alter the variable values as the network progresses. One of the advantages which this model has over most other formal description techniques is that simultaneous transitions are allowed. Another advantage is the use of shared variables rather than FIFO queues for communication between machines. This allows the modeling of the shared medium as a single shared variable variable between all communicating processes. Unlike the SDL language which is used in the specification of the 802.11 standard, the Systems of Communicating Machines model is more compact, easier to understand, and easier to analyze for safety and liveness. (Also UMIACS-TR-2002-36)Item Generalized Fair Reachability Analysis for Cyclic Protocols(1998-10-15) Liu, Hong; Miller, Raymond E.In this paper, the notion of fair reachability is generalized to cyclic protocols with $n\geq 2$ machines. Substantial state reduction can be achieved via fair progress state exploration. It is shown that the fair reachable state space is exactly the set of reachable states with equal channel length. As a result, deadlock detection is decidable for ${\cal P}$, the class of cyclic protocols whose fair reachable state spaces are finite. The concept of simultaneous unboundedness is defined and the lack of it is shown to be a necessary and sufficient condition for a protocol to be in ${\cal P}$. Through finite extension of the fair reachable state space, it is also shown that detection of unspecified receptions, unboundedness, and nonexecutable transitions are all decidable for ${\cal P}$. Furthermore, it is shown that any protocol ${\cal P}$ is logically correct if and only if there is no logical error in its fair reachable state space. This study shows that for the class ${\cal P}$, our generalized fair reachability analysis technique not only achieves substantial state reduction but also maintains very competitive logical error coverage. Therefore, it is a very useful technique to prove logical correctness for a wide variety of cyclic protocols.Item Generalized Fair Reachability Analysis for Cyclic Protocols with Nondeterminism and Internal Transitions(1998-10-15) Liu, Hong; Miller, Raymond E.In this paper, we extend the generalized fair reachability notion to cyclic protocols with nondeterminism and internal transitions. By properly incorporating internal transitions into the formulation of fair progress vectors, we prove that most of the results established for cyclic protocols without nondeterminism and internal transitions still hold even if nondeterminism and internal transitions are allowed. We identify indefiniteness as a new type of logical error resulting from reachable internal execution cycles and show that indefiniteness can also be detected for the class of cyclic protocols with finite fair reachable state spaces with finite extensions.Item On Fault Identification in Networks Using a CFSM Model by Passive Testing(2001-05-10) Miller, Raymond E.; Arisha, Khaled A.In this paper, we employ the Communicating finite state machine (CFSM) model for networks to investigate fault identification using passive testing. First, we introduce the concept of passive testing. Then, we introduce the CFSM model and the observer model with necessary assumptions and justification. We introduce the fault model and the fault detection algorithm using passive testing. Extending our previous work, we develop the new approach for fault identification based on the CFSM model. A 2-node model example is given to illustrate our approach. Then, we illustrate the effectiveness of our new technique through simulation of practical protocol examples, covering both the 2-node and 3-node models. Finally future extensions and potential trends are discussed. (Cross-referenced as UMIACS-TR-2001-28)Item On Fault Location in Networks by Passive Testing(1999-10-09) Miller, Raymond E.; Arisha, Khaled A.In this paper, we employ a variant of the communicating finite state machine (CFSM) model for networks to investigate fault detection and location using passive testing. First, we introduce the concept of passive testing, then we introduce the model with necessary assumptions and justification. Then, the model for the observer process is described and a 3-node case is studied to show how fault location information can be deduced. Extending this result, we propose a multiple node-cut approach for a general network, applying our technique for fault detection and location. An abstraction of a node-cut shows how the 3-node case can be used in the general case. We then illustrate our technique through a simulation of a practical X.25 example. Finally future extensions and potential trends are discussed.Item On Fault Management using Passive Testing for Mobile IPv6 Networks(2001-05-10) Miller, Raymond E.; Arisha, Khaled A.In this paper, we employ the Communicating finite state machine (CFSM) model for networks to investigate fault management using passive testing. First, we introduce the concept of passive testing. Then, we introduce the CFSM model and the observer model with necessary assumptions and justification. We introduce the fault model and the fault detection algorithm using passive testing. We present our new passive testing approach for fault location, fault identification, and fault coverage based on the CFSM model. Examples are given for each fault management function to illustrate our approach. Then, we illustrate the effectiveness of our new technique through simulation of a practical protocol example, a 4-node mobile Ipv6 network. Finally future extensions and potential trends are discussed. (Cross-referenced as UMIACS-TR-2001-15)Item On Hybrid Synthesis for Hierarchical Structured Petri Nets(1998-10-15) Liu, Hong; Park, Jun-Cheol; Miller, Raymond E.We propose a hybrid method for synthesis of hierarchical structured Petri nets. In a top-down manner, we decompose a system into a set of subsystems at each level of abstraction, each of these is specified as a blackbox Petri net that has multiple inputs and outputs. We stipulate that each subsystem satisfies the following I/O constraints: (1) At any instance of time, at most one of the inputs can be activated; and (2) If one input is activated, then the subsystem must consume the input and produce exactly one output within a finite length of time. We give a stepwise refinement procedure which starts from the initial high-level abstraction of the system and expands an internal place of a blackbox Petri net into a more detailed subnet at each step. By enforcing the I/O constraints of each subsystem in each intermediate abstraction, our refinement maintains the sequencing of transitions prescribed by the initial abstraction of the system. Next, for the bottom-up synthesis, we present interconnection rules for sequential, parallel, and loop structures and prove that each rule maintains the I/O constraints. Thus, by incorporating these interconnection rules into our refinement formulation, our approach can be regarded as a hybrid Petri net synthesis technique that employs both top-down and bottom-up methods. The major advantage of the method is that the modeling details can be introduced incrementally and naturally, while the important logical properties of the resulting Petri net are guaranteed.Item Specification and Analysis of the DCF Protocol in the 802.11 Standard using Systems of Communicating Machines(2002-05-22) Vasan, Arunchandar; Miller, Raymond E.The 802.11 specification is an emerging standard for WLANs. In this paper, we propose a formal model for a section of the 802.11 MAC protocol using systems of communicating machines. We model the ad-hoc mode of the DCF, i.e., CSMA/CA protocol and the MACA\footnote{The 802.11 standard does not refer to RTS/CTS exchanges as MACA. However, the paper which introduced this idea called it the MACA, and we use this name.} using RTS/CTS sequences. Each station is modelled as a finite state machine which has a set of local variables, and the Wireless Medium is modelled as a shared variable. Analyses show that the 802.11 MAC CSMA/CA protocol and the MACA using RTS/CTS exchanges are free from state deadlocks and non-executable transitions. However, the MACA protocol has a potential livelock, though it is unlikely it will come to pass in normal operation. (Also UMIACS-TR-2002-37)Item Synthesizing Protocol Specifications from Service Specifications in Timed Extended Finite State Machines(1998-10-15) Park, Jun-Cheol; Miller, Raymond E.We propose a specification model and present a method to algorithmically derive a protocol specification from a service specification based on the model. Unlike the previous models based on finite state machines, the proposed model can explicitly express concurrency, synchronization, and timing requirements such as delays and timeouts. We assume that there exists a reliable communication channel between any two protocol entities and the maximum delay for each channel is bounded by a positive constant. Because of the variable nature of the communication delays along with the time constraints associated with events, no protocol specification can fully simulate the service specification. The proposed method derives a protocol specification that is optimal in the sense that it provides the largest possible subset of the service specification under the communication delay constraints. We also give a method to derive a sub specification from a service specification and a maximum communication delay of each channel such that the sub specification, but no superset of it, can be simulated by the derived protocol specification.