Reports from 1992
Hardware Based Error and Flow Control in the Axon Gigabit Host-Network Interface James P. G. Sterbenz, Anshul Kantawala, Milind Buddhikot, and Gurudatta M. Parulkar
Technical Report
We have proposed a new architecture called Axon that meets the challenges of delivering high performance network bandwidth directly to applications. Its pipelines network interface must perform critical per packet processing in hardware a packets flow through the pipeline, without imposing any store-and-forward buffering of packets. This requires the design of error and flow control mechanisms to be simple enough for implementation in the network interface hardware, while providing functionality required by applications. This paper describes the implementation of the Axon host-network interface, and in particular the hardware design of ...Read More
Hierarchical Correctness Proofs for Recursive Distributed Algorithms using Dynamic Process Creation Bala Swaminathan and Kenneth J. Goldman
Technical Report
We present a new proof methodology that uses dynamic process creation to capture the structure of recutsive distributed algorithms> Each recursive invocation of a distributed algorithm is modeled as a separate process, encouraging local reasoning about the individual recursive invocations and making explicit the communicatino that takes place among the concurrently executing invocations. Our methodology involves the construction of hierarchical correctness proofs in which the state of each individual call in a refined algorithm is mapped to the state of a corresponding call in a simpler or more abstract algorithm. ...Read More
Gesture System for a Graph Editor Burak Muammer Taysi
Technical Report
This thesis investigates a process of designing a gesture system for a simple graphical editor on a pen-based computer. The graphical editor, named Box and Arrow Editor, was developed to test the designed gestures. The results of the testing and the evaluation of the principles used to formulate the gestures are presented. The design process covers issues of application of principles to gesture design, elimination of all menus, user evaluations and recognition problems.
...Read MoreResearch Proposal: Design and Analysis of Practical Switching Networks Ellen E. White
Technical Report
At the heart of any communication system is the switching system for supporting connections between sets of endpoints. A switching system consists of one or more switching networks connected by communication links. Effective design of switching networks is critical to the success of a communication system. This paper proposes the study of three problems in the design of switching networks: design of nonblocking multirate distribution, evaluation of blocking probability in distributors and quantitative comparison of architectures. Each of these problems is significant in the design of practical networks and lacks ...Read More
The Clos Network as a Multirate Distributer with a Greedy Routing Algorithm Ellen E. White
Technical Report
Yang and Masson [14] have demonstrated that the Clos network is a nearly nonblocking distributer, with the proper choice of network parameters. The resulting network has better asymptotic crosspoint compleixty than other known constructions when the number of stages is fixed. In addition, the routing algorithm is efficient, taking time linear in the number of network inputs to route a new connection. We extend these results to the multirate environment in which each connection has an associated weight indicating the fraction of link bandwidth which it requires. Connections may share ...Read More
Multicomputer Checkpointing Ken Wong and Mark Franklin
Technical Report
This paper examines the performance of synchronous checkpointing in a distributed computing environment with and without load redistribution. Performance models are developed, and optimum checkpoint intervals are determined. We extend earlier work by allowing for multiple nodes, state dependent checkpoint intervals, and a performance metric which is coupled with failure-free performance. We show that the optimum checkpoint intervals in the presence of load redestribution has a numerical solution in all cases and a closed form in many reasonable cases. These new results are then used to determine when performance can ...Read More
Reports from 1991
Persistent Connections in High Speed Internets James M. Anderson, Gurudatta M. Parulkar, and Zubin Dittia
Technical Report
We have proposed a very high speed internet (VHSI) abstraction for the next generation of internetwork. An important component of the VHSI is a novel Multipoint Congram-Oriented High Performance Internet Protocol (MCHIP). The congram is the basic service primitive of MCHIP which incorporates strengths of both connection and datagram approaches. MCHIP supports two types of congrams: the user congram (UCon) and the persistent internet congram (PICon). A UCon is similar to a soft connection and can be used to provide strict performance guarantees to applications that need it. PICon are ...Read More
Completely Reliable Auto Shopping Heuristic (CRASH) Todd Bashuk, David Donat, and Kieth Marrs
Technical Report
The major goal of the Completely Reliable Auto Shopping Heuristic (CRASH) system is to simulate a car buying marketplace using belief networks as the inference engine. This paper describes the design, knowledge acquisition, and implementation stages of the CRASH system. The paper also describes the additional work needed to implement CRASH as commercially viable product.
...Read MorePerformance Evaluation of a Traffic Control Mechanism for ATM Networks Andreas D. Bovopoulos
Technical Report
Future ATM networks will be required to support a plethora of services, transaction types and cell sequence behaviors with performance guarantees. Before this goal can be realized, however, some basically problems related to bandwidth allocation and traffic control in the ATM layer must be resolve. Such problems will in all likelihood defy solution as long as they studied in isolation without a unifying traffic characterization and traffic control framework. This work presented in this paper is part of an ongoing effort directed at the development of an integrated traffic characterization ...Read More
Exit Statements are Executable Miracles Wei Chen
Technical Report
In this paper, we present a simple wp semantics and a programming law for the exit statement.
CABeN: A Collection of Algorithms for Belief Networks Steve B. Cousins, William Chen, and Mark E. Frisse
Technical Report
Belief networks have become an increasingly popular mechanism for dealing with uncertainty in systems. Unfortunately, it is known that finding the probability values of belief network nodes given a set of evidence is not tractable in general. Many different simulation algorithms for approximating solutions to this problem have been proposed and implemented. In this report, we describe the implementation of a collection of such algorithms, CABeN. CABeN contains a library of routines for simulating belief networks, a program for accessing the routines through menus on any 'tty' interface, and some ...Read More
The Visual Display of Temporal Information Steve B. Cousins and Michael G. Kahn
Technical Report
The detection of temporal relationships among time-ordered patient data is an important, but difficult, clinical task. Large volumes of computer-stored clinical data offer the possibility of aiding in the early detection of subtle trends and states, but the presence of irrelevant data can obscure relevant findings and relationships. We present a formal system for representing complex temporal data as events on an abstract entity called a time limit. We define five time line operations, SLICE, FILTER, OVERLAY, NEW, and ADD. For each operation, we precisely define the operator's effect on ...Read More
Rapid Display of Radiographic Images Jerome R. Cox Jr., Stephen M. Moore, Robert A. Whitman, G. James Blaine, R. Gilbert Jost, L. Magnus Karlsson, Thomas L. Monsees, Gregory L. Hansen, and Timothy C. David
Technical Report
The requirements for the rapid display of radiographic images exceed the capabilities of widely available display, computer and communication technologies. Computed radiography captures data with a resolution of about four megapixels. Large format displays are available that can present over four megapixels. One megapixel displays are practical for use in combination with large format displays and in areas where the viewing task does not require primary diagnosis. This paper describes an electronic radiology system that approximates the highest quality systems, but through the use of several interesting techniques allows the ...Read More
Project Zeus: Design of a Broadband Network and its Application on a University Campus Jerome R. Cox Jr. and Jonathan S. Turner
Technical Report
This proposal outlines a plan for the design, deployment, and operation of the high speed campus network at Washington University based on fast packet switching technology that has been developed here during the last several years. This new network will support ubiquitous multimedia workstations with high-resolution graphics and video capabilities, opening a wide range of new applications in research and education. It will support aggregate throughputs of hundreds of gigabits per second and will be designed to support port interfaces at up to 2.4 Gb/s. Initial implementations will emphasize 155 ...Read More
SwarmView: A Graphical Engine for the Interpretation and Display of Visualizations Kenneth C. Cox
Technical Report
We have implemented a C-based graphic engine, called SwarmView, which is used to display animation traces as produced by SwarmExec the Prolong-based Swarm execution engine. SwarmView runs on a Silicon Graphics Personal Iris running IRIX, a UNIX-based operating system. This paper describes the major design elements of SwarmView. A basic familiarity with Swarm and its visualization extension is assumed; the interested reader is referred to the referenced papers. Familiarity with the paper "SwarmView Animation Vocabulary and Interpretation" is required; the appendices of this paper are reproduced from that one.
...Read MoreDNA Mapping Algorithms: Fragment Splitting and Combining James Daues and Will Gillet
Technical Report
When using random clone overlap based methods to make DNA maps, fragment matching mistakes, the incorrect matching of similar length restriction fragments, are a common problem that produces incorrect maps. This technical report discusses techniques for fragment splitting and fragment combining, which attempts to correct maps containing a fragment matching mistake, given that the location of the mistake is known. These techniques are based on operations that decompose and merge virtual fragments (a collection of matched real fragments), add virtual fragments to existing groups in the map and insert virtual ...Read More
The Discrete Orthonormal Wavelet Transform: An Introduction Michael Frazier and Arun Kumar
Technical Report
In this paper z-transform theory is used to develop the discrete orthonormal wavelet transpform for multidimensional signals. The tone is tutorial and expository. Some rudimentary knowledge of z-transforms and vector spaces is assumed. The wavelet transform of a signal consists of a sequence of inner products of a signal computed against the elements of a complete orthonorml set of basis vectors. The signal is recovered as a weighted sum of the basis vectors. This paper addresses the necessary and sufficient conditions that such a basis muct respect. An algorithm for ...Read More
The Kumon Approach to Learning Mathematics: An Educator's Perspective Thomas H. Fuller Jr.
Technical Report
Largely unnoticed amid the cry for better mathematics teaching, Kumon is quietly helping a million mathematics students (from infants to adults; 75% are elementary children). Though conservative in diction and device (including 5000+ worksheets to be solved in "standard" times), it is surprisingly student-centered in practice. The author's investigation during the past year reflects his background in both education and computer science. The paper considers the demands, theories, methods and record of Kumon mathematics from the standpoint of educational theory, cognitive science, and language processing. It considers syntactic and semantic ...Read More
Transforming a Rule-based Program Rose F. Gamble
Technical Report
Conflict resolution is a form of global control used in production systems to achieve an efficient sequential execution of a rule-based program. This type of control is not used to parallel production system models [6,13]. Instead, only those programs that make no assumptions regarding conflict resolution are executed in parallel. Therefore, the initial sequential rule-based programs are either executed in parallel without their conflict resolution strategy, which normally results in incorrect behavior, or the programs are transformed in an ad hoc manner to execute on an particular parallel production system ...Read More
Applying Formal Verification Methods to Pure Rule-Based Programs Rose F. Gamble, Gruia-Catalin Roman, William E. Ball, and H. Conrad Cunningham
Technical Report
Reliability, defined as the guarantee that a program satisfies its specifications, is an important aspect of many applications for which rule-based expert systems are suited. Verification refer to the process used to determine the reliability of the rule-based program. Because past approaches to verification are informal, guarantees of reliability cannot fully be made without severely restricting the system. On the other hand, by constructing formal specifications for a program and showing the program satisfies those specifications, guarantees of reliability can be made. This paper presents an assertional approach to the ...Read More
DNA Mapping Algorithms: Abstract Data Types - Concepts and Implementation Will Gillett and Liz Hanks
Technical Report
The conceptual aspects of and the implementation details of a set of self-identifying abstract data types (ADT) are described. Each of the ADTs constitutes a specific class of object, upon which a set of well-defined access functions is available. The intent of these ADTs is to supply a paradigm in which a class of object is available for manipulation, but in which the underlying implementation is hidden from the application programmer. Specific ADTs are the described in some detail. The tagged architecture used to achieve the self-identifying property of the ...Read More
Composition, Superposition, and Encapsulation in the Formal Specification of Distributed Systems Kenneth J. Goldman
Technical Report
Composition, superposition, and encapsulation are important techniques that work well together for designing large distributed software systems. Composition is a symmetric operator that allows system components to communicate with each other across module boundaries. Superposition is an asymmetric relationship that allows one system component to observe the state of another. Encapsulation is the ability to define the reason about the behavior of a module in terms of a well-defined boundary between that module and its environment, while hiding the internal operations of that module. In this paper, the I/O automation ...Read More
The Spectrum Simulation System: A Formal Approach to Distributed Algorithm Development Tools Kenneth J. Goldman
Technical Report
We present the Spectrum Simulation System, a new research tool for the design and study of distributed algorithms. Based on the formal Input/Output Automation model of Lynch and Tuttle, Spectrum allows one to express distributed algorithms as collections of I/O automata and simulate them directly in terms of the semantics of that model. This permits integration of algorithm specification, design, debugging, analysis, and proof of correctness within a single formal framework that is natural for describing distributed algorithms. Spectrum provides a language for expressing algorithms as I/O automata, a simulator ...Read More
Computational Learning Theory Lecture Notes for CS 582 Spring Semester, 1991 Sally A. Goldman
Technical Report
This manuscript is a compilation of lecture notes from the graduate level course CS 582, "Computational Learning Theory," I taught at Washington University in the spring of 1991. Students taking the course were assumed to have background in the design and analysis of algorithms as well as good mathematical background. Given that there is no text available on this subject, the course material was drawn from recent research papers. I selected the first twelve topics and the remainder were selected by the students from a list of provided topics. This ...Read More
Exact Identification of Read-once Formulas Using Fixed Points of Amplification Functions Sally A. Goldman, Michael J. Kearns, and Robert E. Schapire
Technical Report
In this paper we describe a new technique for exactly identifying certain classes of read-once Boolean formulas. The method is based on sampling the input-output behavior of the target formula on a probability distribution which is determined by the fixed point of the formula's application function (defined as the probability that a 1 is output by the formula when each input bit is 1 independently with probability p). By performing various statistical tests on easily sampled variants of the fixed-point distribution, we are able to efficiently infer all structural information ...Read More
The Difficulty of Random Attribute Noise Sally A. Goldman and Robert H. Sloan
Technical Report
This paper studies the robustness of pac learning algorithms when the instance space is {0,1}n, and the examples are corrupted by purely random noise affecting only the instances (and not the labels). In the past, conflicting results on this subject have been obtained-- the "best agreement" rule can only tolerate small amounts of noise, yet in some cases large amounts of noise can be tolerated. We show the truth lies somewhere between the two alternatives. For uniform attribute noise, in which each attribute is flipped independently at random with the ...Read More
The Power of Self-Directed Learning Sally A. Goldman and Robert H. Sloan
Technical Report
This paper studies self-directed learning, a variant of the on-line learning model in which the learner selects the presentation order for the instances. We give tight bounds on the complexity of self-directed learning for the concept classes of monomials, k-term DNF formulas, and orthogonal rectangles in {0, 1, . . ., n-1}d. These results demonstrate that the number of mistakes under self-directed learning can be surprisingly small. We then prove that the model of self-directed learning is more powerful than all other commonly unused on-line and query learning models. Next ...Read More
A Recurrence Model for Asynchronous Pipeline Analysis Fengmin Gong, Zubin Dittia, and Gurudatta M. Parulkar
Technical Report
This paper presents an analytical model for performance analysis of asynchronous pipelines based on recurrence relations. The model accurately describes the behavior of an asynchronous pipeline, yet yields to very efficient computations. It has been implemented and verified using discrete event simulations. Results of the verification experiments are also described. We also outline a number of ways that the proposed recurrence model can be used to gain insight into many issues concerning engineering of asynchronous pipelines.
...Read MoreEfficient Queries For Quasi-Ordered Databases Victor Jon Griswold
Technical Report
The problem of selecting database tuples is central to the task of resolving many forms of queries. The report defines a class of selection queries and presents a set of algorithms for their efficient resolution. The class of queries investigated is those queries which impose a quasi order on the tuples in a database.
A Parser Generator Based on Earley's Algorithm Jawaid Hakim
Technical Report
Most parser generators are programs that take a context-free grammar specification for a language and generate a parser for that language. Usually, the parsers generated by these parser generators are based on some variations of LL(k) or LR(k) parsing algorithms. The parser generators discussed in this paper creates parsers based on Earlcy's Algorithm. This parser generator creates parsers from any arbitrary context-free grammar specifications; even from ambiguous, cyclic, and unbounded look ahead grammar. These parsers are more powerful than LL(k) and LR(k) parsers and enable the user to create many ...Read More
Ranking Radiotherapy Treatment Plans using Decision-Analytic and Heuristic Techniques Nilesh L. Jain and Michael G. Kahn
Technical Report
Radiotherapy treatment optimization is done by generating a set of tentative treatment plans, evaluating them and selecting the plan closest to achieving a set of conflicting treatment objectives. The evaluation of potential plans involves making tradeoffs among competing possible outcomes. Multiattribute decision theory provides a framework for specifying such tradeoffs and using them to select optimal actions. Using these concepts, we have developed a plan-ranking model which ranks a set of tentative treatment plans from best to worst. Heuristics are used to refine this model so that it reflects the ...Read More
Quicksort in Constant Space Anne Kaldewaij and Jan Tijmen Udding
Technical Report
An in situ sorting algorithm, based on Quicksort, is presented with its proof of correctness. The proof illustrates a concise and elegant way to represent a sequence that has been partially sorted by Quicksort. A list representation turns out to be well suited to this purpose, and the discussion is entirely in terms of lists.
Rank Order Filters and Priority Queues Anne Kaldewaij and Jan Tijmen Udding
Technical Report
A derivation of a parallel algorithm for rank order filtering is presented. Both derivation and result differ from earlier designs: the derivations are less complicated and the result allows a number of different implementations. The same derivation is used to design a collection of priority queues. Both filters and priority queues are highly efficient: they have constant response time and small latency.
...Read MoreDesign of an ATM-FDDI Gateway Sanjay Kapoor and Gurudatta M. Parulkar
Technical Report
Asynchronous transfer mode (ATM) networks are capable of supporting a wide variety of applications with varying data rates. FDDI networks offer to support similar applications in the LAN environment. Both these networks are characterized by high data rates, low error rates, and are capable of providing performance guarantees. In this paper we present the design of an ATM-FDDI gateway that can provide high performance internetworking between these two important classes of networks. An important part of the gateway design philosophy is to partition the functionality into critical and non-critical paths. ...Read More
An Access Protection Solution for Heavy Load Unfairness in DQDB Lakshmana N. Kumar and Andreas D. Bovopoulos
Technical Report
This paper discusses the unfairness issue arising in a 802.6 DQDB network at high loads-- when the traffic demand to a bus exceeds the capacity of that bus. As per the 802.6 protocol, at heavy loads, the end nodes along a bus experience longer delays than the other nodes. The origin and remedy of this heavy load unfairness is discussed. An access control scheme is proposed as a solution. The comparison of the proposed scheme with 802.6 protocol is presented. The simulation results and performance characteristics are discussed under several ...Read More
DNA Mapping Algorithms: Clone Sequencing Judith H. Lewis and Will Gillett
Technical Report
The DNA restriction mapping problem can be abstracted to the Shortest Common Matching String problem by viewing the restriction fragment lengths as symbols and the clones as bags. The Shortest Common Matching String problem can be decomposed into the Bag Sequencing problem and the Symbol Sequencing problem. All three of these problems have bene shown to be NP-hard. Rhee has proposed a family of greedy algorithms to compute polynomial time approximations to the Bag Sequencing problem, which produced surprisingly good performance results on abstracted data. In the test data generated ...Read More
SAAM: The Strategic Asset Allocation Model Judy Lewis, Todd Gamble, and John Tai
Technical Report
Asset Allocation has become a dominant factor for investment strategies in recent years. It has found that by holding a strategically diversified portfolio, a high total return on investments can be maintained while, at the same time, reducing portfolio volatility. With recent federal regulations mandating pension investment responsibilities, appropriate asset allocation has become more important than ever. SAAM is a software package specifically designed to be used as a tool to aid the investment professional in determining pension portfolio allocations. SAAM uses the expect system shell CLIPS, has a user-friendly ...Read More
Performance Analysis of the Ethernet under Conditions of Bursty Traffic Tony Y. Mazraani and Gurudatta M. Parulkar
Technical Report
In this paper we present a simulation study of the Ethernet performance under conditions of bursty traffic. This study is motivated by two observations: Ethernet will continue to be a widely used Local Area Network (LAN), especially as an access LAN for future high speed internet (or Broadband ISDN); and future high speed applications can best be modeled as bursty sources. Bursty traffic in this study is specified using three parameters: peak bandwidth, average bandwidth, and burst factor. The simulation study shows that the inherent behavior of the Ethernet does ...Read More
DNA Mapping Algorithms: Topological Mapping Kenneth Moorman, Paul Poulosky, and Will Gillett
Technical Report
There are several basic approaches that can be used in attempting to produce high-resolution DNA restriction maps. A standard approach is the match/merge approach in which first the topology of the map units being mapped together is suppressed and lists of potential matches between fragments are generated, and second the topology is introduced to eliminate matchlists which are inconsistent with the topology. This technical report documents a different approach to DNA mapping, known as topological mapping. In topological mapping the precedence of the two criteria are reversed, i.e., the topology ...Read More
Remote Visualization: Challenges and Opportunities Panel Statement Gurudatta M. Parulkar
Technical Report
Converting Binary Thresholds Networks into Equivalent Symmetric Networks Gadi Pinkas
Technical Report
We give algorithms to convert any network of binary threshold units (that does not oscillate) into an equivalent network with symmetric weight matrix (like Hopfield networks [Hopfield 82] or Boltzmann machines [Hinton, Sejnowski 88]). The motivation for the transformation is dual: a) to demonstrate the expressive power of symmetric networks; i.e. binary threshold networks (that do not oscillate) are subsumed in the energy minimization paradigm; 2) to use network modules (developed for the spreading activation paradigm for example), within the energy minimization paradigm. Thus optimization [Tank, Hopfield 88] and approximation ...Read More
First-Order Logic Proofs using Connectionist Constraints Relaxation Gadi Pinkas
Technical Report
This paper considers the problem of expressing predicate calculus in connectionist networks that are based on energy minimization. Given a first-order-logic knowledge base and a bound k, a symmetric network is constructed (like a Boltzman machine or a Hopfield network) that searches for a proof fora given query. If a resolution-based proof is length no longer k exists, then the global minima of the energy function that is associated with the network represent such proofs. If no proof exist then the global minima indicate the lack of a proof. The ...Read More
Propositional Non-Monotonic Reasoning and Inconsistency in Symmetric Neural Networks Gadi Pinkas
Technical Report
We define a notion of reasoning using world-rank-functions, independently of any symbolic language. We then show that every symmetric neural network (like Hopfield networks or Boltzman machines) can be seen as performing a search for a satisfying model of some knowledge that is wired into the network's topology and weights. Several equivalent languages are then shown to describe symbolically the knowledge embedded in these networks. We extend propositional calculus by augmenting assumptions with penalties. The extended calculus (called "penalty logic") is useful in expressing default knowledge, preference between arguments, and ...Read More
Representation and Learning of Propositional Knowledge in Symmetric Connectionist Networks Gadi Pinkas
Technical Report
The goal of this article is to construct a connectionist inference engine that is capable of representing and learning nonmotonic knowledge. An extended version of propositional calculus is developed and is demonstrated to be useful for nonmonotonic reasoning and for coping with inconsistency that may be a result of noisy, unreliable sources of knowledge. Formulas of the extended calculus (called penalty logic) are proved to be equivalent in a very strong sense to symmetric networks (like Hopfield networks and Boltzmann machines), and efficient algorithms are given for translating back and ...Read More
Symmetric Neural Nets and Propositional Logic Satisfiability Gadi Pinkas
Technical Report
Connectionist networks with symmetric weights (like Hopfield networks and Boltman Machines) use gradient descent to find a minimum for quadratic energy functions. We show an equivalence between the problem of satisfiability in propositional calculus and the problem of minimizing those energy functions. The equivalence is in the sense that for an satisfiable Well Formed Formula (WFF) we can find a quadratic function that describes it, such that the set of solutions that minimize the function is equal to the set of truth assignments that satisfy the WFF. We also show ...Read More
Reasoning for Inconsistency-- A Taxonomy and a Connectionist Approach Gadi Pinkas and Ron P. Loui
Technical Report
A consequence relation (CR) relates sets of beliefs to the appropriate conclusions that might be deduced. Of special interest to Artificial Intelligence are CRs that cope with inconsistency within the set of beliefs. Default reasoning, belief revision, social choice and reasoning from conflicting knowledge sources are just a few examples of mechanisms that need to handle inconsistency, In this paper we show a taxonomy in which many existing mechanisms are mapped, and new interesting ones are revealed. We identify simple relations among the CRs and give a language for their ...Read More
Pavane: A System for Declarative Visualization of Concurrent Computations Gruia-Catalin Roman, Kenneth C. Cox, C. Donald Wilcox, and Jerome Y. Plum
Technical Report
This paper describes the conceptual model, specification method, and visualization methodology for Pavane-- a visualization environment concerned with exploring, monitoring, and presenting concurrent computations. The underlying visualization model is declarative in the sense that visualization is treated as a mapping from program states to a three-dimensional world of geometric objects. The latter is rendered in full color and may be examined freely by a viewer who is allowed to navigate through the geometric world. The state-to-geometry mapping is defined as a composition of several simpler mappings. The choice is determined ...Read More
Reasoning about Synchronic Groups Gruia-Catalin Roman and H. Conrad Cunningham
Technical Report
Swarm is a computational model which extends the UNITY model in three important ways: (1) UNITY's fixed set of variables is replaced by an unbounded set of tuples which are addressed by content rather than by name; (2) UNITY's static set of statements is replaced by a dynamic set of transactions; and (3) UNITY's state II-composition is augmented by dynamic coupling of transactions into synchronic groups. This last feature, unique to Swarm, facilitates formal specification of the mode of execution (synchronous or asynchronous) associated with portions of a concurrent program ...Read More
Formal Derivation of Rule-Based Program Gruia-Catalin Roman, Rose F. Gamble, and William E. Ball
Technical Report
This paper describes a formal approach to developing concurrent rule-based programs. Our program derivation strategy starts with a formal specification of the problem. Specification refinement is used to generate an initial version of the program. Program refinement is then applied to produce a highly concurrent and efficient version of the same program. Techniques for the deriving concurrent programs through either specification or program refinement have been described in previous literature. The main contribution of this paper consists of extending the applicability of these techniques to a broad class of rule-based ...Read More
Formal Verification of Pure Production Systems Programs Gruia-Catalin Roman, Rose F. Gamble, and William E. Ball
Technical Report
Reliability, defined as the guarantee that a program satisfies its specifications, is an important aspect of many applications for which rule-based expert systems are suited. Executing rule-based programs on a series of test cases. To show a program is reliable, it is desirable to construct formal specifications for the program and to prove that it obeys those specifications. This paper presents an assertional approach to the verification of a class of rule-based programs characterized by the absence of conflict resolution. The proof logic needed for verification is already in use ...Read More