Follow


Reports from 1992

PDF

Proposal for a comprehensive bandwidth management scheme and connection acceptance rule for B-ISDN Giuseppe Bianchi and Vittorio Trecordi
Technical Report

Abstract:

A feasible and cost-effective resource management scheme is urgently needed in the Broadband Integrated Services Digital Network adopting the Asynchronous Transfer Mode (ATM) technique. In this paper we propose a simple and comprehensive strategy to manage bandwidth allocations, congestion control and quality of service (QOS) integrity in a multi-service ATM network. The proposed framework involves a core network that grants a limited number of grade of service (GOS) profiles and suggest the design of edge-adaptors able to match QOS user's requirements with associated connection acceptance algorithms are presented. Also, for ...Read More

PDF

Improved Queueing Analysis of Shared Buffer Switching Networks Giuseppe Bianchi and Jonathan S. Turner
Technical Report

Abstract:

This paper describes several methods for analyzing the queueing behavior of switching networks with flow control and shared buffer switches. It compares the various methods on the basis of accuracy and computation speed, where the performance metric of the most concern is the maximum throughput. The best of the methods accurately predicts throughput for multi-stage networks constructed from large switches (greater than equal to 8 ports).

...Read More

PDF

Exact and Approximate Solution of a Multiplexing Problem Mario Bonatti, Andreas Bovopoulos, Apostolos Dailianas, and Alexei Gaivoronski
Technical Report

Abstract:

In this paper the detailed solution of the multiplexing problem of independent but not necessarily homogenous traffic sources is presented. The "curse of dimensionality" of problems of realistic dimensions is comprehensively addressed by a methodology employing state aggregation. A number of detailed examples provide further insight into the multiplexing problems and their exact and approximate solutions.

...Read More

PDF

Optimal Burst Level Admission Control In A Broadband Network Andreas D. Bovopoulos
Technical Report

Abstract:

In a broadband ATM network the traffic of a virtual circuit is defined at the cell, burst and call levels. All virtual circuits sharing the resources of a switch are statistically multiplexed at the cell level. In this paper the issue of how to control the admission of bursts of a particular virtual circuit is analyzed. It is demonstrated that under two optimization criteria, the optimal burst level admission control of a virtual circuit is a window control. This result suggests that while the cells of all virtual circuits sharing ...Read More

PDF

Statistical Multiplexing of Semi-Markov Modulated Sources Andreas D. Bovopoulos and Saied Hosseini-Khayat
Technical Report

Abstract:

It is shown that when a continuous buffer is driven by a semi-Markox modulated fluid flow source(s), the stationary distribution of the buffer content is governed by the same differential equation describing the distribution for continuous time Markov modulated fluid source(s) [1]. It is also shown that the same techniques can be utilized to decompose and solve the eigenvalue problem associated with the differential equation [6]. Finally it is shown that the stationary distribution of buffer content depends only on the mean time spent by each multiplexed semi-Markov source in ...Read More

PDF

The Effect of Delayed Feedback Information on Network Performance Andreas D. Bovopoulos and Aurel A. Lazar
Technical Report

Abstract:

The performance of a network subject to either state dependent or state independent flow control is investigated. In the state dependent case, the flow control policy is a function of the total number of packets for which the controller has not yet received an acknowledgement. In this case it is shown that the optimal flow control is a sliding window mechanism. The effect of the delayed feedback on the network performance as well as the size of the window are studied. The state independent optimal rate is also derived. The ...Read More

PDF

Simulation of an ATM-FDDI Gateway Milind M. Buddhikot, Sanjay Kapoor, and Gurudatta M. Parulkar
Technical Report

Abstract:

Asynchronous transfer mode (ATM) networks can support a wide variety of applications with varying data rates. Fiber Distributed Data Interface (FDDI) networks are targeted to support similar applications, but only in a LAN environment. Both of these networks are characterized by high data rates and low error rates. In addition, they can provide applications with varying degrees of performance guarantees. A problem of designing a high-performance gateway architecture for internetworking between these two important classes of networks was addressed in [Kapoor, 1991b]. An important part of the gateway design philosophy ...Read More

PDF

Inversion Laws for Specifications and Recursive Procedures Wei Chen
Technical Report

Abstract:

In this paper, we continue the work on the formal approach to program inversion by presenting programming laws for specifying the inverse program according to the specification of its forward program, and for inverting recursive procedues. The formal establishment of these laws, once more, convinces us that program inversion has nice mathematical properties that can be used in formal program development. Some examples are included to illustrate the usage of the laws developed in this paper.

...Read More

PDF

Project Zeus: Design of a Broadband Network and its Application on a University Campus Jerome R. Cox Jr., Michael E. Gaddis, and Jonathan S. Turner
Technical Report

Abstract:

This is a report of the results of the initial step in a plan for the design, deployment and operation of a high speed campus network at Washington University. The network is based on ATM switching technology that has been developed here during the last several years. This network will support ubiquitous multimedia workstations with high-resolution graphics and video capabilities, open up 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 ...Read More

PDF

CtoVis: An Interface between C Programs and Pavane Visualizations Kenneth C. Cox
Technical Report

Abstract:

PDF

Abstraction in Algorithm Animation Kenneth C. Cox and Gruia-Catalin Roman
Technical Report

Abstract:

Abstraction of information into visual form plays a key role in the development of algorithm animations. We present a classification for abstraction as applied to algorithm animation. The classification emphasizes the expressive power of the abstraction, ranging from simple direct presentation of the program's state to complex animations intended to explain the behavior of the program. We illustrate our classification by presenting several visualizations of a shortest path algorithm.

...Read More

PDF

Experiences with the Pavane Program Visualization Environment Kenneth C. Cox and Gruia-Catalin Roman
Technical Report

Abstract:

The Pavane system is an implementation of the declarative visualization model, which treats visualization as a mapping form the state of some entity (a program, an execution, a data set, etc.) to images. We briefly discuss the declarative visualization model and the implementation of Pavane. We then present some of the results that we have obtained with Pavane. These results are divided into three parts: a discussion of the development of visualizations focusing on the roles played by the various participants, a critique of declarative visualization in general and Pavane ...Read More

PDF

An Implementation Model for Connection-Oriented Internet Protocols Charles D. Cranor and Gurudatta M. Parulkar
Technical Report

Abstract:

Recently a number of research groups have proposed connection-oriented access protocols that can provide a variable grade of service with performance guarantees on top of diverse networks. These connection-oriented internet protocols (COIPs) have different performance trade-offs. The purpose of this paper is to create a COIP-Kernel which can be used as a toolkit to implement any of the proposed COIPs. COIP-K features module interchanges and incremental software support. The paper presents the COIP-K implementation and its performance characterization.

...Read More

PDF

Formal Specifications and Design of a Message Router Christian Creveull and Gruia-Catalin Roman
Technical Report

Abstract:

Formal derivation refers to a family of design techniques that entail the development of programs which are guaranteed to be correct by construction. This paper investigates the possible application of one such technique-- UNITY-style specification refinement-- to industrial-grade problems. The formal specification and design of a message router illustrates the derivation process and helps identify those methodological elements that are likely to contribute to successful use of this technique in industrial environment. Although, the message router cannot be characterized as being industrial-grade, it is a sophisticated problem that pose significant ...Read More

PDF

Efficient Accommodation of May-Alias Information in SSA Form Ron Cytron and Reid Gershbein
Technical Report

Abstract:

We present an algorithm for incrementally including may-alias information into Static Single Assignment form by computing a sequence of increasingly precise (and correspondingly larger) partial SSA forms. Our experiments show significant speedup of our method over exhaustive use of may-alias information, as optimization problems converge well before most may-aliases are needed.

...Read More

PDF

Connection Management Access Protocol (CMAP) Specification John DeHart, Mike Gaddis, and Rick Bubenik
Technical Report

Abstract:

This document specifies a Connection Management Access Protocol (CMAP) for managing multipoint connectinos in high-speed packet switched networks. We target CMAP to networks employing the Asynchronous Transfer Mode (ATM) communication standard. We define a multipoint connection as a communication channel between two or more clients of the network, where all data sent by one client is received by all other clients who have elected to receive. A point-to-point connection is a special case of a multipoint connection involving only two clients. CMAP specifies the access procedures exercised by clients to ...Read More

PDF

Algorithms for Designing Nonblockings Communication Networks with General Topologies J. Andrew Fingerhut
Technical Report

Abstract:

A framework is given for specifying nonblocking traffic requirements in a connection-oriented communications network. In this framework, connections may be form one point to one other point, or they may involve multiple points. Different connections may have different data rates. The communication networks are constructed from switches (or nodes) and trunks, which connect pairs of switches. This framework is intended to model Asynchronous Transfer Mode (ATM) networks and traffic. Several computational problems are formulated, each intended to find a minimum cost configuration of switches and trunks which satisfy given traffic ...Read More

PDF

Designing Communication Networks with Fixed or Nonblocking Traffic Requirements J. Andrew Fingerhut
Technical Report

Abstract:

A general framework for specifying communication network design problems is given. We analyze the computational complexity of several specific problems within this framework. For fixed multirate traffic requirements, we prove that a particular network analysis problem is NP-complete, although several related network design problems are either efficiently solvable or have good approximation algorithms. For the case when we wish the network to operate without blocking any connection requests, we give efficient algorithms for dimensioning the link capacities of the network.

...Read More

PDF

Performance Comparison of Clocked and Asynchronous Pipelines Mark A. Franklin and Tienyo Pan
Technical Report

Abstract:

Clock (synchronous) and self-timed (asynchronous) represent the two principal methodologies associated with timing control and synchronization of digital systems. In this paper, clocked and the asynchronous instruction and arithmetic pipelines are modeled and compared. The approach, which yields the best performance is dependent on technology parameters, operating range and pipeline algorithm characteristics. Design curves are presented which permit selection of the best approach for a given application and technology environment.

...Read More

PDF

Energy-related Feature Abstraction for Handwritten Digit Recognition Thomas H. Fuller Jr.
Technical Report

Abstract:

Most handwritten character recognizers use either graphical (static) or first-order dynamic data. Our research speculates that the mental signal to write a digit might be partially encoded as an energy profile. We used artificial neural networks (ANN) to analyze energy-related features (first and second time derivatives) of handwritten digits of 20 subjects and later 40 subjects. An experimenal environment was developed on a NeXTstation with a real-time link to a pen-based GO computer. Although such an experiment cannot confirm an energy profile encoded in the writer, it did indicate the ...Read More

PDF

DNA Mapping Algorithms: Strategies for Single Restriction Enzyme and Multiple Restriction Enzyme Mapping Will Gillett
Technical Report

Abstract:

An approach to high-resolution restriction-fragment DNA mapping, known as Multiple-Restriction-Enzyme mapping (MRE mapping), is present. This approach significantly reduces the uncertainty of clone placement by using clone ends to synchronize the position in of clones within different maps, each map being constructed from fragment-length data produced by digestion of each clone with a specific restriction enzyme. Maps containing both fragments-length data and clone-end data are maintained for each restriction enzyme, and synchronization between two such maps is achieved by requiring them to have "compatible" clone-end map projections. Basic definitions of ...Read More

PDF

Separating Structure from Function in the Specification and Design of Distributed Systems Kenneth J. Goldman
Technical Report

Abstract:

A distributed system is viewed as a collection of functional components and a unifying structure that defines relationships among the components. In the paper, we advocate a particular approach to distributed system specification and design in which the structure of a distributed system is specified separately from the functional components. This permits one to reason about individual functional components in isolation, and encourages one to make explicit not only the input/output behavior of the functional components but also the logical placement of these components within the overall structure of the ...Read More

PDF

The Programmers' Playground: I/O Abstraction for Heterogeneous Distributed Systems Kenneth J. Goldman and Michael D. Anderson
Technical Report

Abstract:

A new high-level approach to interprocess communication in heterogeneous distributed systems in introduced, This approach, called I/O Abstraction, allows one to write each functional component of a distributed system as an encapsulated program that acts upon a set of local data structures, some of which may be published for external use. The functional components are separately configured by establishing logical connections among the published data structures. In order to illustrate this approach, we describe the The Programmers' Playground, a high-level language "veneer" and protocol designed to support I/O abstraction in ...Read More

PDF

On the Complexity of Teaching Sally A. Goldman and Michael J. Kearns
Technical Report

Abstract:

While most theoretical work in machine learning has focused on the complexity of learning, recently there has been increasing interest in formally studying the complexity of teaching. In this paper we study the complexity of teaching by considering a variant of the on-line learning model in which a helpful teacher selects the instances. We measure the complexity of teaching a concept from a given concept class by a combinatorial measure we call the teaching dimension. Informally, the teaching dimension of a concept class is the minimum number of instances a ...Read More

PDF

On the Sample Complexity of Weakly Learning Sally A. Goldman, Michael J. Kearns, and Robert E. Schapire
Technical Report

Abstract:

In this paper, we study the sample complexity of weak learning. That is, we ask how much data must be collected from an unknown distribution in order to extract a small but significant advantage in prediction. We show that it is important to distinguish between those learning algorithms that output deterministic hypotheses and those that output randomized hypotheses. We prove that in the weak learning model, any algorithm using deterministic hypotheses to weakly learn a class of Vapnik-Chervonenkis dimension d(n) requires (omega) (square root of d(n) examples.

...Read More

PDF

Learning k-term DNF Formulas with an Incomplete Oracle Sally A. Goldman and H. David Mathais
Technical Report

Abstract:

We consider the problem of learning k-term DNF formulas using equivalence queries and incomplete membership queries as defined by Angluin and Slonim. We demonstrate the this model can be applied to non-monotone classes. Namely, we describe a polynomial algorithm that exactly identifies a k-term DNF formula with a k-term DNF hypothesis using incomplete membership queries and equivalence queries from the class of DNF formulas.

...Read More

PDF

Can PAC Learning Algorithms Tolerate Random Attribute Noise? Sally A. Goldman and Robert H. Sloane
Technical Report

Abstract:

This paper studies the robustness of pac learning algorithms when the instances 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 that the truth lies somewhere in between these two alternatives. For uniform attribute noise, in which each attribute is flipped independently at ...Read More

PDF

The Power of Self-Directed Learning Sally A. Goldman and Robert H. Sloan
Technical Report

Abstract:

This paper studies self-directed learning, a variant of the on-line (or incremental) learning model in which the learner selects the presentation order for the instances. Alternatively, one can view this model as a variation of learning with membership queries in which the learner is only "charged" for membership queries for which it could not predict the outcome. We give tight bounds on the complexity of self-directed learning for the concept classes of monomials, monotone DNF formulas, and axis-parallel rectangles in {0,1 ' ' ', n-1}d. These results demonstrate that the ...Read More

PDF

An Application-Oriented Error Control Scheme for High Speed Networks Fengmin Gong and Guru Parulkar
Technical Report

Abstract:

Many new network applications demand interprocess communication (IPC) services that are not supported by existing transport network protocol mechanisms. Large bandwidth-delay products of high-speed networks also render the existing error control mechanism inefficient. This paper presents the design, evaluation, and implementations of an application-oriented error control scheme that can support efficient IPC for these applications in high-speed network environments.

...Read More

PDF

A Two-Level Flow Control Scheme for High Speed Networks Fengmin Gong and Guru Parulkar
Technical Report

Abstract:

Many new network applications demand interprocess communication (IPC) services with guaranteed bandwidth, delay, and low. Existing transport protocol mechanisms have not been designed with these service objectives. Large bandwidth-delay products of high-speed networks also render the existing flow control mechanism inefficient. This paper presents the design, evaluation, and implementation of a two-level flow control scheme that can support efficient IPC for these applications in high-speed network environments.

...Read More

PDF

An Overview of Segment Streaming for Efficient Pipelined Televisualization Fengmin Gong and Gurudatta M. Parulkar
Technical Report

Abstract:

The importance of scientific visualization for both science and engineering endeavors has been well recognized. Televisualization becomes necessary because of the physical distribution of data, computation resources, and users invovled in the visualization process. However, televisualization is not adequately supported by existing communication protocols. We believe that a pielined televisualization model (PTV) is suitable for efficient implementation of most visualization applications. In order to support this model over high speed networks, we are developing a segment streaming interprocess communication (IPC) mechanism within the Axon communication architecture. Important aspects of this ...Read More

PDF

Design of a Multimedia Applications Development System Raman Gopalakrishnan and Andreas D. Bovopoulos
Technical Report

Abstract:

The application envisaged for high speed packet switched networks have diverse and demanding transport requirements that are not satisfied by current communications software implementations. In addition, existing communication interfaces for distributed programs are not general enough to express the communication patterns and control required for distributed applications. This Multimedia Applications Development (MAD) system is designed to address these problems mentioned above. It is intended as a platform for implementing and experimenting with protocols and their implementation, network service access methods, and communication primitives for constructing distributed multimedia applications. It is ...Read More

PDF

Exact Dominance without Search in Decision Trees Nilesh L. Jain and Ronald P. Loui
Technical Report

Abstract:

In order to improve understanding of how planning and decision analysis relate, we propose a hybrid model containing concepts from both. This model is comparable to [Hartman90], with slightly more detail. Dominance is simple concept in decision theory. In a restricted version of our model, we give conditions under which dominance can be detected without search: that is, it can be used as a pruning strategy to avoid growing large trees. This investigation follows the lead of [Wellman87]. The conditions seem hard to meet, but may nevertheless be useful in ...Read More

PDF

Hyperflow: A Uniform Visual Language for Different Levels of Programming Takayuki Dan Kimura
Technical Report

Abstract:

We propose a visual language, Hyperflow, for system programming as well as for end user shell programming. Hyperflow is designed for a multimedia pen computer system for children. It is a dataflow-based graphical language similar to Show and Tell. In order to demonstrate the capability of Hyperflow, we solve the programming problem of implementing a help command for children to telephone their instructor or parents using voice communication hardware (modem, microphone, speaker, and a clock). The resulting program includes visual programs to implement device drivers for the modem and clock ...Read More

PDF

Hyperflow: A Visual Programming Language for Pen Computers Takayuki Dan Kimura
Technical Report

Abstract:

This paper presents the design philosophy of the Hyperflow visual programming language. It also gives an overview of its semantic model. The primary purpose of language is to provide a user interface for a pen-based multimedia computer system designed for school children. Yet it is versatile enough to be used as a system programming language. The concept of visually interactive process, vip in short, is introduced as the fundamental element of the semantics. Vips communicate with each other through exchange of signals, either discrete or continuous. Each vip communicates with ...Read More

PDF

Kumon Machine: Learning Math with Silicon Paper Takayuki Dan Kimura
Technical Report

Abstract:

PDF

A Protocol for Dynamic Assessment of Network Topology in DQDB MANs Lakshmana N. Kumar and Andreas D. Bovopoulos
Technical Report

Abstract:

The 802.6 protocol of DQDB MANs aims to maintain a distributed queue for network access and yet inherits access unfairness. In this paper, the DANT protocol is proposed to provide head-end nodes as well as each active node in a DQDB network with real time information about the active node population, the intermodal distance, the position of each node along what bus and the length of a node's downstream bus segment. DANT's current implementation introduces an overhead of 5 bits per slot but alternative implementations which retain the current slot ...Read More

PDF

The 3-Tier Structured Access Protocol to Control Unfairness in DQDB MANs Lakshmana N. Kumar and Andreas D. Bovopoulos
Technical Report

Abstract:

This paper addresses the unfairness problem appearing in 802.6-based DQDB MANs. Traffic load demand is characterized as low (below 0.4 of the channel capacity), normal (from 0.4 to 0.9 of the channel capacity) or heavy (greater than 0.9 of the channel capacity). At low loads the 802.6 protocol is acceptably fair. At normal loads, however, the protocol performance is markedly unfair. The unfairness is related to the latency in transporting a request. At heavy loads the unfairness is both latency-related and flooding-related. In this paper, both types of unfairness are ...Read More

PDF

An Argument Game Ronald Loui and William Chen
Technical Report

Abstract:

This game was designed to investigate protocols and strategies for resource-bounded disputation. The rules presented here correspond very closely to the problem of controlling search in an actual program.

PDF

Computing Specificity Ronald Loui, J. Norman, K. Stiefvater, A. Merrill, A. Costello, and J. Olson
Technical Report

Abstract:

This note reports on an effort to implement a version of Poole's rule for specificity. Relatively, efficient implementation relies on correcting and improving a pruning lemma of Simari-Loui [92]. This in turn requires revision of Poole's specificity concept. The resulting system is a usable knowledge representation system with first-order-language and defeasible reasoning. Sample input and output are included in an appendix. It is a good candidate for multiple inheritance applications; it is useful for planning, but limited by the underlying search for plans.

...Read More

PDF

Process and Policy: Resource-Bounded Non-Demonstrative Reasoning Ronald P. Loui
Technical Report

Abstract:

This paper investigates the appropriateness of formal dialectics as a basis for non-monotonic and defeasible reasoning that takes computational limits seriously. Rules that can come into conflict should be regarded as policies, which are inputs to deliberative processes. Dialectical protocols are appropriate for such deliberations when resources are bounded and search is serial. AI, it is claimed here, is now perfectly positioned to correct many misconceptions about reasoning that have resulted from mathematical logic's enormous success in this century: among them (1) that all reasons are demonstrative, (2) that rational ...Read More

PDF

A Model for Detecting Motifs in Biological Sequences Andrew F. Neuwald and Phillip P. Green
Technical Report

Abstract:

A method for detecting patterns in biological sequences is described that incorporates rigorous statistics for determining significances, and an algebraic system that, in combination with a depth first search procedure, can be used to efficiently search for all patterns up to a specified length. This method includes a context free command language grammar and is formulated using a mathematical model amendable to additions enhancements, The method was implemented and verified by detection of various types of patterns in protein sequences.

...Read More

PDF

Experimental Evaluation of SUNOS IPC and TCP/IP Protocol Implementations Christos Papadopoulos and Gurudatta M. Parulkar
Technical Report

Abstract:

Progress in the field of high speed networking and distributed applications has led to the debate in the research community on suitability of existing protocols such as TCP/IP for emerging applications over high speed networks. Protocols have to operate in a complex environment comprising of various operating systems, host architectures, and a rapidly growing and evolving internet of large number of heterogeneous subnetworks. Thus, evaluation of protocols is definitely a challenging task and cannot be achieved by studying protocols in isolation. This paper presents results of a research project that ...Read More

PDF

An Improved Activation Function for Energy Minimization Gadi Pinkas and Rina Dechter
Technical Report

Abstract:

Symmetric networks that are based on energy minimization, such as Boltzmann machines or Hopfield nets, are used extensively for optimization, constraint satisfaction, and approximation of NP-hard problems. Nevertheless, finding a global minimum for the energy function is not guaranteed, and even a local minimum may take an exponential number of steps. We propose and improvement to the standard activation function used for such networks. The improved algorithm guarantees that a global minimum is found in linear time for tree-like subnetworks. The algorithm is uniform and does not assume that the ...Read More

PDF

Pavane User's Manual Jerome Y. Plun
Technical Report

Abstract:

This report describes the Pavane visualization system. Pavane is set to a set of tools allowing on to 1) simulate the execution of a computation specified with the Swarm model and 2) visualize the state of the computation by mean of a set of rules. Pavane also provides the means to visualize other computations. This manual describes how to initiate a Pavane session to visualize a Swarm computation as well as the role of each of the component of such as session.

...Read More

PDF

Swarm Language Reference Manual Jerome Y. Plun, C. Donald Wilcox, and Kenneth C. Cox
Technical Report

Abstract:

This document contains a description of the grammar and syntax rules of the Swarm programming language. This language, which is an implementation of the program specification language used with the Swarm computational model, is used both to specify programs and their visualizations, for the use of the Pavane program visualization system.

PDF

Program Visualization: The Art of Mapping Programs to Pictures Gruia-Catalin Roman and Kenneth C. Cox
Technical Report

Abstract:

In this paper program visualization is defined as a mapping from programs to graphical representations. Simple forms of program visualization are frequently encountered in software engineering. For this reason current advances in program visualization are likely to influence future developments concerning software engineering tools and environments. This paper provides a new taxonomy of program visualization research. The proposed taxonomy becomes the vehicle through which we carry out a systematic review of current systems, techniques, trends, and ideas in program visualization.

...Read More

PDF

Seeking Concurrency in Rule-based Programming Gruia-Catalin Roman, Rose F. Gamble, and William E. Ball
Technical Report

Abstract:

This paper describes a formal approach for developing concurrent rule-based programs. Specification of 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 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 programs. To the best of our knowledge, this is the first time ...Read More

PDF

Architecture-Directed Refinement Gruia-Catalin Roman and C. Donald Wilcox
Technical Report

Abstract:

As critical computer systems continue to grow in complexity, the task of demonstrating that they are correct, that is, guaranteed to operate without failure, becomes more difficult. For this reason, research in software engineering has turned to formal methods, i.e. rigorous approaches to demonstrating the correctness of software systems. Unfortunately, the formal methods currently used for concurrent systems do no provide a mechanism for expressing and manipulating non-functional constraints formally. In this paper, we show that one class of non-functional constraints, the target architectures, can be expressed using formal notation ...Read More

PDF

On Deriving Distributed Programs from Formal Specifications of Functional Requirements and Architectural Constraints Gruia-Catalin Roman, C. Donald Wilcox, and Jerome Y. Plum
Technical Report

Abstract:

This design of distributed programs is a difficult task which can greatly benefit from the application of formal methods. Since design solutions are determined not only by functional requirements imposed by the application but also by the structure and behavior of the underlying hardware architecture, a complete formal treatment of the program derivation process becomes a significant challenge. The common approach is to state with a formal specification of the functional requirements and to derive the desired program through systematic refinements which factor in the architectural constraints informally, in an ...Read More