Reports from 1992
Proposal for a comprehensive bandwidth management scheme and connection acceptance rule for B-ISDN Giuseppe Bianchi and Vittorio Trecordi
Technical Report
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
Improved Queueing Analysis of Shared Buffer Switching Networks Giuseppe Bianchi and Jonathan S. Turner
Technical Report
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 MoreExact and Approximate Solution of a Multiplexing Problem Mario Bonatti, Andreas Bovopoulos, Apostolos Dailianas, and Alexei Gaivoronski
Technical Report
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 MoreOptimal Burst Level Admission Control In A Broadband Network Andreas D. Bovopoulos
Technical Report
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
Statistical Multiplexing of Semi-Markov Modulated Sources Andreas D. Bovopoulos and Saied Hosseini-Khayat
Technical Report
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
The Effect of Delayed Feedback Information on Network Performance Andreas D. Bovopoulos and Aurel A. Lazar
Technical Report
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
Simulation of an ATM-FDDI Gateway Milind M. Buddhikot, Sanjay Kapoor, and Gurudatta M. Parulkar
Technical Report
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
Inversion Laws for Specifications and Recursive Procedures Wei Chen
Technical Report
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 MoreProject 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
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
CtoVis: An Interface between C Programs and Pavane Visualizations Kenneth C. Cox
Technical Report
Abstraction in Algorithm Animation Kenneth C. Cox and Gruia-Catalin Roman
Technical Report
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 MoreExperiences with the Pavane Program Visualization Environment Kenneth C. Cox and Gruia-Catalin Roman
Technical Report
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
An Implementation Model for Connection-Oriented Internet Protocols Charles D. Cranor and Gurudatta M. Parulkar
Technical Report
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 MoreFormal Specifications and Design of a Message Router Christian Creveull and Gruia-Catalin Roman
Technical Report
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
Efficient Accommodation of May-Alias Information in SSA Form Ron Cytron and Reid Gershbein
Technical Report
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 MoreConnection Management Access Protocol (CMAP) Specification John DeHart, Mike Gaddis, and Rick Bubenik
Technical Report
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
Algorithms for Designing Nonblockings Communication Networks with General Topologies J. Andrew Fingerhut
Technical Report
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
Designing Communication Networks with Fixed or Nonblocking Traffic Requirements J. Andrew Fingerhut
Technical Report
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 MorePerformance Comparison of Clocked and Asynchronous Pipelines Mark A. Franklin and Tienyo Pan
Technical Report
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 MoreEnergy-related Feature Abstraction for Handwritten Digit Recognition Thomas H. Fuller Jr.
Technical Report
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
DNA Mapping Algorithms: Strategies for Single Restriction Enzyme and Multiple Restriction Enzyme Mapping Will Gillett
Technical Report
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
Separating Structure from Function in the Specification and Design of Distributed Systems Kenneth J. Goldman
Technical Report
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
The Programmers' Playground: I/O Abstraction for Heterogeneous Distributed Systems Kenneth J. Goldman and Michael D. Anderson
Technical Report
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
On the Complexity of Teaching Sally A. Goldman and Michael J. Kearns
Technical Report
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
On the Sample Complexity of Weakly Learning Sally A. Goldman, Michael J. Kearns, and Robert E. Schapire
Technical Report
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 MoreLearning k-term DNF Formulas with an Incomplete Oracle Sally A. Goldman and H. David Mathais
Technical Report
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 MoreCan PAC Learning Algorithms Tolerate Random Attribute Noise? Sally A. Goldman and Robert H. Sloane
Technical Report
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
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 (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
An Application-Oriented Error Control Scheme for High Speed Networks Fengmin Gong and Guru Parulkar
Technical Report
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 MoreA Two-Level Flow Control Scheme for High Speed Networks Fengmin Gong and Guru Parulkar
Technical Report
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 MoreAn Overview of Segment Streaming for Efficient Pipelined Televisualization Fengmin Gong and Gurudatta M. Parulkar
Technical Report
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
Design of a Multimedia Applications Development System Raman Gopalakrishnan and Andreas D. Bovopoulos
Technical Report
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
Exact Dominance without Search in Decision Trees Nilesh L. Jain and Ronald P. Loui
Technical Report
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
Hyperflow: A Uniform Visual Language for Different Levels of Programming Takayuki Dan Kimura
Technical Report
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
Hyperflow: A Visual Programming Language for Pen Computers Takayuki Dan Kimura
Technical Report
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
Kumon Machine: Learning Math with Silicon Paper Takayuki Dan Kimura
Technical Report
A Protocol for Dynamic Assessment of Network Topology in DQDB MANs Lakshmana N. Kumar and Andreas D. Bovopoulos
Technical Report
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
The 3-Tier Structured Access Protocol to Control Unfairness in DQDB MANs Lakshmana N. Kumar and Andreas D. Bovopoulos
Technical Report
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
An Argument Game Ronald Loui and William Chen
Technical Report
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.
Computing Specificity Ronald Loui, J. Norman, K. Stiefvater, A. Merrill, A. Costello, and J. Olson
Technical Report
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 MoreProcess and Policy: Resource-Bounded Non-Demonstrative Reasoning Ronald P. Loui
Technical Report
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
A Model for Detecting Motifs in Biological Sequences Andrew F. Neuwald and Phillip P. Green
Technical Report
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 MoreExperimental Evaluation of SUNOS IPC and TCP/IP Protocol Implementations Christos Papadopoulos and Gurudatta M. Parulkar
Technical Report
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
An Improved Activation Function for Energy Minimization Gadi Pinkas and Rina Dechter
Technical Report
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
Pavane User's Manual Jerome Y. Plun
Technical Report
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 MoreSwarm Language Reference Manual Jerome Y. Plun, C. Donald Wilcox, and Kenneth C. Cox
Technical Report
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.
Program Visualization: The Art of Mapping Programs to Pictures Gruia-Catalin Roman and Kenneth C. Cox
Technical Report
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 MoreSeeking Concurrency in Rule-based Programming Gruia-Catalin Roman, Rose F. Gamble, and William E. Ball
Technical Report
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
Architecture-Directed Refinement Gruia-Catalin Roman and C. Donald Wilcox
Technical Report
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
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
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