Author

D Luckham

51 papers · 1964–2018

1964peak 4 in 19802018

Frequent co-authors

Papers

showing 1–25 of 51 RSS

Specification and analysis of system architecture using Rapide

D Luckham, J.J. Kenney, Larry M. Augustin +3 more

Computer Networks and Communications · IEEE Transactions on Software Engineering · April 1995 · cited 762× · DOI ↗ · more like this ·

Rapide is an event-based, concurrent, object-oriented language specifically designed for prototyping system architectures. Two principle design goals are: (1) to provide constructs for defining executable prototypes of architectures and (2) to adopt an execution model in which the concurrency, synchronization, dataflow, and timing properties of a prototype are explicitly represented. This paper describes the partially ordered event set (poset) execution model and outlines with examples some of the event-based features for defining communication architectures and relationships between architectures. Various features of Rapide are illustrated by excerpts from a prototype of the X/Open distributed transaction processing reference architecture.< <ETX xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">></ETX>

An event-based architecture definition language

D Luckham, Jose Belisario Vera Vera

Artificial Intelligence · IEEE Transactions on Software Engineering · 1995 · cited 485× · DOI ↗ · more like this ·

This paper discusses general requirements for architecture definition languages, and describes the syntax and semantics of the subset of the Rapide language that is designed to satisfy these requirements. Rapide is a concurrent event-based simulation language for defining and simulating the behavior of system architectures. Rapide is intended for modelling the architectures of concurrent and distributed systems, both hardware and software in order to represent the behavior of distributed systems in as much detail as possible. Rapide is designed to make the greatest possible use of event-based modelling by producing causal event simulations. When a Rapide model is executed it produces a simulation that shows not only the events that make up the model's behavior, and their timestamps, but also which events caused other events, and which events happened independently. The architecture…

Debugging Ada Tasking Programs

D. Heimbold, D Luckham

Hardware and Architecture · IEEE Software · March 1985 · cited 202× · DOI ↗ · more like this ·

Debuggers for parallel programs have to be more than passive information gatherers-they should automatically detect errors. Powerful task debuggers for Ada can be constructed by extending existing tools that detect deadlock.

The Power of Events: An Introduction to Complex Event Processing in Distributed Enterprise Systems

D Luckham

Computer Networks and Communications · Lecture notes in computer science · 2008 · cited 95× · OpenAlex ↗ · more like this ·

Complex Event Processing (CEP) is a defined set of tools and techniques for analyzing and controlling the complex series of interrelated events that drive modern distributed information systems. This emerging technology helps IS and IT professionals understand what is happening within the system, quickly identify and solve problems, and more effectively utilize events for enhanced operation, performance, and security. CEP can be applied to a broad spectrum of information system challenges, including business process automation, schedule and control processes, network monitoring and performance prediction, and intrusion detection. This talk is about the rise of CEP as we know it today, its historical roots and its current position in commercial markets. Some possible long-term future roles of CEP in the Information Society are discussed along with the need to develop rule-based event…

Verification of Array, Record, and Pointer Operations in Pascal

D Luckham, Norihisa Suzuki

Artificial Intelligence · ACM Transactions on Programming Languages and Systems · October 1979 · cited 74× · DOI ↗ · more like this ·

A practical method is presented for automating in a uniform way the verification of Pascal programs that operate on the standard Pascal data structures Array, Record, and Pointer. New assertion language primitives are introduced for describing computational effects of operations on these data structures. Axioms defining the semantics of the new primitives are given. Proof rules for standard Pascal operations on data structures are then defined using the extended assertion language. An axiomatic rule for the Pascal storage allocation operation, NEW, is also given. These rulers have been implemented in the Stanford Pascal program verifier. Examples illustrating the verification of programs which operate on list structures implemented with pointers and records are discussed. These include programs with side effects.

Ada exception handling: an axiomatic approach

D Luckham, Wolfgang Polak

Artificial Intelligence · ACM Transactions on Programming Languages and Systems · April 1980 · cited 68× · DOI ↗ · more like this ·

A method of documenting exception propagation and handling in Ada programs is proposed. Exception propagation declarations are introduced as a new component of Ada specifications, permitting documentation of those exceptions that can be propagated by a subprogram. Exception handlers are documented by entry assertions. Axioms and proof rules for Ada exceptions given. These rules are simple extensions of previous rules for Pascal and define an axiomatic semantics of Ada exceptions. As a result, Ada programs specified according to the method can be analyzed by formal proof techniques for consistency with their specifications, even if they employ exception propagation and handling to achieve required results (i.e., nonerror situations). Example verifications are given.

Three Concepts of System Architecture

D Luckham, James Vera, Sigurd Meldal

Information Systems · July 1995 · cited 44× · OpenAlex ↗ · more like this ·

Abstract An architecture is a specification of the components of a system and the communication between them. Systems are constrained to conform to an architecture. An architecture should guarantee certain behavioral properties of a conforming system, i.e., one whose components are configured according to the architecture. An architecture should also be useful in various ways during the process of building a system. This paper presents three alternative concepts of architecture: object connection architecture, interface connection architecture, and plug and socket architecture. We describe different concepts of interface and connection that are needed for each of the three kinds of architecture, and different conformance requirements of each kind. Simple examples are used to compare the usefulness of each kind of architecture in guaranteeing properties of conforming systems, and in…

A type system for prototyping languages

Dinesh Katiyar, D Luckham, John C. Mitchell

Hardware and Architecture · 1994 · cited 44× · DOI ↗ · more like this ·

RAPIDE is a programming language framework designed for the development of large, concurrent, real-time systems by prototyping. The framework consists of a type language and default executable, specification and architecture languages, along with associated programming tools. We describe the main features of the type language, its intended use in a prototyping environment, and rationale for selected design decisions.

ANNA

Bernd Krieg Brückner, D Luckham

Artificial Intelligence · 1980 · cited 31× · DOI ↗ · more like this ·

ANNA is a proposal to extend Ada to include facilities for formally specifying the intended behaviour of Ada programs (or portions thereof) at all stages of program development. ANNA programs are Ada programs with formal comments. Formal comments in ANNA consist of virtul Ada text and annotations. The syntax and semantics of different kinds of annotations are defined: declarative annotations (for variables, subtypes, subprograms, and packages), statement annotations, exception annotations, and visibility annotations. ANNA includes a small number of predefined attributes which may appear only in annotations, e.g., access type collections.

TSL

David P. Helmbold, D Luckham

Hardware and Architecture · ACM SIGAda Ada Letters · May 1985 · cited 28× · DOI ↗ · more like this ·

TSL is a language for specifying sequences of tasking events in Ada 1 programs. TSL specifications are submitted with an Ada program and are monitored at runtime for consistency with the actual tasking events as they occur. This paper presents a preliminary design for TSL, an informal overview of its capabilities, and an operational semantics.

A methodology for verifying programs

F. W. von Henke, D Luckham

Artificial Intelligence · ACM SIGPLAN Notices · April 1975 · cited 25× · DOI ↗ · more like this ·

The paper investigates methods for applying an online interactive verification system designed to prove properties of PASCAL programs. The methodology provides techniques for developing a debugged and verified version starting from an incomplete program .

Two-dimensional pinpointing: debugging with formal specifications

D Luckham, Syam Sankar, Satoshi Takahashi

Information Systems · IEEE Software · 1991 · cited 24× · DOI ↗ · more like this ·

Debugging techniques and tools that draw on both the high-level concepts (defined as functions) used in formal specifications and the abstraction and information-hiding constructs used in modern languages are described. The technique is based on two components. One is a novel specification language with support tools. Ada programs are specified with a language that the authors created called Anna. Their tool set is used to check the Ada program's runtime behavior for consistency with the Anna specifications. The other technique uses the tool set to find missing specifications by comparing the specification with program prototypes and to test and debug Ada programs after an accepted specification has been developed. The approach, called two-dimensional pinpointing, locates inconsistencies in software that is structured in levels.< <ETX xmlns:mml="http://www.w3.org/1998/Math/MathML"…

A new approach to prototyping Ada-based hardware/software systems

Frank C. Belz, D Luckham

Hardware and Architecture · 1990 · cited 24× · DOI ↗ · more like this ·

Prototyping is not a single technique, but rather a collection of widely diverse activities, with highly fragmented support technology. TRW and Stanford have recently collaborated to develop an approach for reducing this fragmentation in the future. This approach is particularly supportive of the development of large distributed systems in Ada. It is based upon the design of a prototyping language and system which we are tentatively calling Reality. The Reality language is a departure from “normal” programming languages, but bears similarities in form and concepts to standard languages Ada and VHDL. In fact, it can be viewed as both

On automating the construction of programs.

Jack R. Buchanan, D Luckham

Artificial Intelligence · May 1974 · cited 20× · OpenAlex ↗ · more like this ·

An experimental system for automatically generating certain simple kinds of programs is described. The programs constructed are expressed in a subset of ALGOL containing assignments, function calls, conditional statements, while loops, and non-recursive procedure calls. The input is an environment of primitive programs and programming methods specified in a lnaugage currently used to define the semantics of the output programming language. The system has been used to generate programs for symbolic manipulation, robot control, every day planning, and computing arithmetical functions.

Enlisting event patterns for cyber battlefield awareness

Louis Perrochon, Eunhei Jang, Stephane Kasriel +1 more

Computer Networks and Communications · 7 Nov 2002 · cited 18× · DOI ↗ · more like this ·

Cyber warfare consists to a large degree of reaction to activities happening in the information infrastructure. Better knowledge of the status of this infrastructure at any time allows more appropriate reactions. Context-based event correlation can provide a more appropriate view of the cyber battlefield by providing users a view on the desired level of abstraction. We informally introduce context as the temporal and causal relations between events. Event correlation based on event patterns in a declarative language means we specify what to detect, instead of how to detect. We describe the Stanford University context-based event correlator that is able to process events on-line, as they are generated. It can be reconfigured dynamically while it is running. On the example of intrusion detection, we show how Complex Event Processing (CEP) increases detection rate, reduce false alarms, and…

Verification of VHDL designs using VAL

Larry M. Augustin, Benoit A. Gennart, Youm Huh +2 more

Hardware and Architecture · Design Automation Conference · June 1988 · cited 18× · DOI ↗ · more like this ·

VAL (VHDL Annotation Language) uses a small number of new language constructs to annotate VHDL hardware descriptions. VAL annotations, added to the VHDL entity declaration in the form of formal comments, express intended behavior common to all architectural bodies of the entity. Annotations are expressed as parallel processes that accept streams of input signals and generate constraints on output streams. VAL views signals as streams of values ordered by time. Generalized timing expressions allow the designer to refer to relative points on a stream. No concept of preemptive delayed assignment or inertial delay are needed when referring to different relative points in time on a stream. The VAL abstract state model permits abstract data types to be used in specifying history dependent device behavior. Annotations placed inside a VHDL architectural body define detailed correspondences…

Monitoring for deadlocks in Ada tasking

Steven M. German, David P. Helmbold, D Luckham

Hardware and Architecture · 6 Oct 1982 · cited 18× · DOI ↗ · more like this ·

Most high level languages with multiprocessing do not have built in mechanisms to detect deadlocks during program execution. We present transformation rules for taking an original Ada program P and deriving a new program P', such that P' has a potential deadlock iff P does, and P' signals whenever a deadlock is about to occur. In principle, the transformations can be applied mechanically, giving a practical tool for debugging deadlocks. Since this method modifies the source program, it can be used with any implementation of the language, without special knowledge of the implementation of tasking. The transformations that we have developed thus far are sufficient to handle most of the complexities of Ada tasking, including arbitrary task types, conditional entry calls, selective waits, timed entry calls, and intertask exceptions.

Automatic runtime consistency checking and debugging of formally specified programs

D Luckham, Sriram Sankar

Software · 1989 · cited 17× · OpenAlex ↗ · more like this ·

This thesis studies an approach to automate the process of deciding whether a program is performing correctly, and if not, to discover the probable cause of the problem. It assumes that the intended behavior of the program is specified in some formal, high-level specification language. It studies how one can check automatically at runtime whether the program is running consistently with its specification, and if not, how inconsistencies can be automatically detected and diagnosed. A methodology of using this checking methodology for debugging formally specified programs is then presented. The consistency checking methodology depends on the particular specification language constructs used. In this thesis, two categories of constructs are studied: (1) generalized assertions and (2) algebraic specifications. Generalized assertions contain boolean expressions that must be satisfied…

Runtime detection and description of deadness errors in Ada tasking

David P. Helmbold, D Luckham

Hardware and Architecture · ACM SIGAda Ada Letters · May 1985 · cited 13× · DOI ↗ · more like this ·

A runtime monitoring system for detecting and describing tasking errors in Ada programs is presented. Basic concepts for classifying tasking errors, called deadness errors, are defined. These concepts indicate which aspects of an Ada computation must be monitored in order to detect deadness errors resulting from attempts to rendezvous or terminate. They also provide a basis for the definition and proof of correct detection. Descriptions of deadness errors are given in terms of the basic concepts. The monitoring system has two parts: (1) a separately compiled runtime monitor that is added to any Ada source text to be monitored, and (2) a pre-processor that transforms the Ada source text so that necessary descriptive data is communicated to the monitor at runtime. Some basic preprocessing transformations and an abstract monitoring for a limited class of errors were previously presented.

Adam: An Ada‐based language for multiprocessing

D Luckham, F. W. von Henke, Howard J. Larsen +1 more

Computer Networks and Communications · Software Practice and Experience · July 1984 · cited 13× · DOI ↗ · more like this ·

Abstract Adam is a high‐level language for parallel processing. It is intended for programming resource scheduling applications, in particular supervisory packages for run‐time scheduling of multiprocessing systems. An important design goal was to provide support for implementation of Ada and its run‐time environment. Adam has been used to implement Ada task supervision and also as a high‐level target language for compilation of Ada tasking. Adam provides facilities corresponding to the Ada sequential constructs (including subprograms, packages, exceptions, generics). In addition, it provides specialized module constructs for implementation of packages that may be shared between parallel processes, and new predefined types for scheduling. The parallel processing constructs of Adam are more primitive than Ada tasking. Strong restrictions are enforced on the ways in which parallel…

Polymorphism and subtyping in interface

Dinesh Katiyar, D Luckham, John C. Mitchell

Hardware and Architecture · 1994 · cited 11× · DOI ↗ · more like this ·

RAPIDE is a programming language framework designed for the development of large, concurrent, real-time systems by prototyping. The framework consists of a type language and default executable, specification and architecture languages, along with associated programming tools. Interfaces are the central construct of the type system. This document describes RAPIDE interfaces, their expressiveness and their use as a typing construct.

An environment for Ada software development based on formal specification

D Luckham, Randall Neff, David S. Rosenblum

Artificial Intelligence · ACM SIGAda Ada Letters · May 1987 · cited 9× · DOI ↗ · more like this ·

This report gives an overview of the current status and plans to construct a prototype environment of advanced tools for software and hardware development based on the use of wide-spectrum languages. The wide-spectrum languages include Anna (ANNotated Ada), and TSL (Task Sequencing Language). The tools described here provide interactive aid at all stages in the system development process. Special emphasis is placed on distributed computing, both in providing tools for handling parallelism in the subject system, and in designing tools that utilize parallelism in the programming environment. Applications of these tools include requirements analysis, formal specification, rapid prototyping, testing, formal verfication and construction of self-testing Ada software for multi-processor systems.The report describes an existing environment of prototype tools supporting applications of Anna and…

Verification of fairness in an implementation of monitors

Richard Alan Karp, D Luckham

Artificial Intelligence · International Conference on Software Engineering · 13 Oct 1976 · cited 9× · DOI ↗ · more like this ·

An implementation in Pascal by Saxena and Bredt of the Monitor construct is studied. Techniques are given for using a program verifer to analyse the conditions under which the implementation is fair (i.e. once a process is delayed it eventually will be continued). By use of a virtual data structure, fairness is represented in terms of simple properties which can be verified automatically.Examples are given illustrating how the verification can force unstated assumptions upon which the implementation depends to be made explicit, and how it can be used to study whether the implementation makes adequate use of resources. The development of techniques for analysis of such implementations is required before the correctness of high-level language operating systems such as Brinch Hansen's SOLO can be completely established.

Automatic generation of programs containing conditional statements

D Luckham, Jack R. Buchanan

Artificial Intelligence · Artificial Intelligence and the Simulation of Behaviour · July 1974 · cited 9× · OpenAlex ↗ · more like this ·

An experimental system for automatically generating certain simple kinds of programs is described. The programs constructed are expressed in a subset of ALGOL containing assignments, function calls, conditional statements, while loops, and non-recursive procedure calls. The system has been used to generate programs for symbolic manipulation, robot control, every day planning, and computing arithmetical functions. This system has previously been described in [Buchanan and Luckham 1974]. The present report focuses on the generation of conditional statements and describes applications to mechanical assembly and symbolic manipulation problems.

Two Dimensional Pinpointing: An Application of Formal Specification to Debugging Packages

D Luckham

Software · April 1989 · cited 8× · DOI ↗ · more like this ·

Inservice training to promote health education is important and, for it to be truly effective, teachers must be intimately involved from the beginning. This article describes the operation of the Portal School Program at Arizona State University which is one method for promoting health education in elementary schools. The program is easy to implement and has been shown to be effective. The program uses a three-phase approach of development, dissemination, and review. It provides for the development of teacher designed health education materials, promotes the use of these materials in the classroom, and provides a mechanism for their review and refinement.