VTechWorks staff will be away for the Thanksgiving holiday beginning at noon on Wednesday, November 27, through Friday, November 29. We will resume normal operations on Monday, December 2. Thank you for your patience.

Browsing by Author "Lee, John A.N."

Now showing 1 - 4 of 4
  • Thumbnail Image
    AdaTAD - a debugger for the Ada multi-task environment
    Fainter, Robert Gaffney (Virginia Polytechnic Institute and State University, 1985)
    In a society that is increasingly dependent upon computing machinery, the issues associated with the correct functioning of that machinery are of crucial interest. The consequences of erroneous behavior of computers are dire with the worst case scenario being, conceivably, global thermonuclear war. Therefore, development of procedures and tools which can be used to increase the confidence of the correctness of the software that controls the world's computers is of vital importance. The Department of Defense (DoD) is in the process of adopting a standard computer language for the development of software. This language is called Ada¹. One of the major features of Ada is that it supports concurrent programming via its "task" compilation unit. There are not, however, any automated tools to aid in locating errors in the tasks. The design for such a tool is presented. The tool is named AdaTAD and is a debugger for programs written in Ada. The features of AdaTAD are specific to the problems of concurrent programming. The requirements of AdaTAD are derived from the literature. AdaTAD is, however, a unique tool designed using Ada as a program description language. When AdaTAD is implemented in Ada it becomes portable among all environments which support the Ada language. This offers the advantage that a single debugger is portable to many different machine architectures. Therefore, separate debuggers are not necessary for each implementation of Ada. Moreover, since AdaTAD is designed to allow debugging of tasks, AdaTAD will also support debugging in a distributed environment. That means that, if the tasks of a user's program are running on different computers in a distributed environment, the user is still able to use AdaTAD to debug the tasks as a single program. This feature is unique among automated debuggers. After the design is presented, several examples are offered to explain the operation of AdaTAD and to show that AdaTAD is useful in revealing the location of errors specific to concurrent programming.
  • Thumbnail Image
    Integrating formal specification and verification methods in software development
    He, Xudong (Virginia Polytechnic Institute and State University, 1989)
    This dissertation is a part of an intended long-term research project with the objectives to make software development more scientific and rigorous, thereby to achieve better software quality and to facilitate automated software production; and has two major components: the design of the specification transition paradigm for software development and the theoretical study of the system specification phase in the paradigm. First, after an extensive analysis and comparison of various formalisms, a paradigm for integrating various formal specification and verification methods (predicate transition Petri nets, first order temporal logic, the algebraic, the axiomatic, the denotational, and the operational approaches) in software development has been developed. The model more effectively incorporates foremost formalisms than any other models (the Automatic Programming Project [Bal85], the CIP Project [ClP85], the Larch Project [GHW85] and the RAISE Project [MG87]) and has the following distinctive features: (1) specifications are viewed both as a set of products and a set of well-defined steps of a process, (2) specifications (as a set of products) at different development steps are to be written and verified by different formalisms, (3) specification (as a process) spans from the requirement phase to the detailed design phase, (4) specification for both concurrent and sequential software is supported, and (5) specifications for different aspects (concurrent control abstraction, data abstraction, and procedural abstraction) of a piece of software are dealt with separately. Second, an intensive and in-depth investigation of the system specification phase in the paradigm results in: - a design methodology for predicate transition nets, which incorporates the separate definition technique in Ada [Ada83] and state decomposition technique in Statechart [Har88] into the traditional transformation techniques for Petri nets, and therefore will significantly reduce the design complexity and enhance the comprehensibility of large predicate transition net specifications; - the establishment of a fundamental relationship between predicate transition nets and first order temporal logic and the design of an algorithm for systematically translating predicate transition nets into equivalent temporal logic formulae. Therefore the goal to combine the strengths of both formalisms, i.e. to use predicate transition nets as a specification method and to use temporal logic as a verification method, is achieved; and - the discovery of a special temporal logic proof technique based on a Hilbert-style logic system to verify various properties of predicate transition nets and the associated theorems. Thus temporal logic is effectively used as an analysis method for both safety and liveness properties of predicate transition nets.
  • Thumbnail Image
    Polymorphic types for constructing concurrent objects and layered communication protocols
    Lavender, R. Gregory (Virginia Tech, 1993-05-05)
    Polymorphic type abstractions are proposed for constructing concurrent objects and layered peer-to-peer communication protocols, both of which exhibit inherently asynchronous behavior. The type abstractions are shown to be both expressive and efficient in the context of a statically typed object-oriented language. Where appropriate, the utility of the type abstractions is illustrated by demonstrating their usefulness in concurrent programming using the Actor model. The results of this work have direct applicability to problems in concurrent programming, distributed systems, and communication protocol architectures. An extensible, polymorphic type abstraction for structuring concurrent method execution in a strongly typed object-oriented language is introduced. The type abstraction is called a polymorphic lambda type. A lambda type is an abstraction for a procedure that is based in part on λ-abstraction in the λ-calculus. The lambda type is a key component of a concurrent object model that allows methods defined in a class to be instantiated as lambda objects. Lambda objects are used to represent some aspect of behavior and they represent a first-class execution environment. The first-class nature of lambda objects facilitates the construction of more powerful computational abstractions, primarily those requiring 'asynchronous interaction and concurrent execution. Through a series of refinements, lambda objects are shown to be as expressive as traditional procedures with little extra cost for call setup and invocation. Concurrent objects require synchronization control. A type abstraction called a behavior set is introduced for specifying synchronization constraints in a strongly typed concurrent object-oriented language with Actor-style concurrency semantics. The behavior set abstraction offers a solution to structuring synchronization control that coexists with an inheritance mechanism, thereby avoiding the inheritance anomaly.
  • Thumbnail Image
    Specification of multi-object coordination schemes using coordinating environments
    Mukherji, Manibrata (Virginia Tech, 1995)
    This dissertation proposes a coordination model for concurrent object-oriented programming languages (COOPLs). The model, termed Coordinating Environments (CEs), prescribes coordination among concurrently executing objects that compute as a group to achieve a common task or goal. The model represents coordination constraints and coordinating actions in a structured manner by grouping them into syntactic entities called Coordinating Behaviors (CBs). A group coordinator, termed a Coordinating Environment object (CE object), reduces the intrusive effects of coordination by transparently observing message-acceptance and method-termination events in components and triggering one or more coordinating actions on them. The conflict between the issues of information hiding (for better encapsulation) and information externalization (to enable coordination) is partially resolved by requiring components to provide state-interrogation methods. This allows a CE object to obtain and use local state information of components for the purpose of coordination. A method for developing reusable coordination specifications in C++ is described. The method consists of two major steps: defining an abstract Coordinating Environment class (CE class) to capture the coordination problem in an abstract manner and then defining a concrete CE class (a subclass of the abstract CE class) to map the coordination effect embodied in the abstract CE class to a specific coordination problem. The method makes extensive use of the inheritance, polymorphism, and dynamic binding mechanisms of C++. Seven coordination problems, ranging from the coordination of a panel of buttons to the coordination of a multi-car elevator system, are specified to illustrate the method. A detailed design of the major components of the CEs model is also described. The issues involved in using formal abstractions for coordinating process-agents specified in the Calculus of Communicating Systems (CCS) are also investigated. Using CCS directly to specify coordination has two weaknesses. First, coordination is modeled at a very low level in CCS by making agents engage in explicit communications. Such low-level specifications are poor candidates for specifying designs of software components that must satisfy software engineering criteria such as separation of concerns and reusability. Second, when the computation steps of the composition of agents are determined using the Expansion Law of CCS, many terms are generated that represent incorrect coordination sequences among the agents. Thus, the need for a calculus that addresses both the issue of concurrency and communication and the issue of effectively managing the communication among concurrent agents (that is, coordination) is identified, and the Calculus of Coordinating Environments (CCE) is proposed as a first step towards satisfying that need.