Selected Publications of
Laura K. Dillon

These documents are made available as a means to ensure timely dissemination of scholarly and technical work on a non-commercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each copyright holder. These works may not be reposted without the explicit permission of the copyright holder.

A Component-Oriented Model for the Design of Safe Multi-threaded Applications, Reimer Behrends, R. E. K. Stirewalt and L. K. Dillon, Proc. 2005 International SIGSOFT Symposium on Component-based Software Engineering (CBSE 2005), Lecture Notes in Computer Science 3489, May 2005, pp. 251—267.

Abstract: We previously developed a component-oriented model that combines ideas from self-organizing architectures and from design by contract to address the complexity of design in multi-threaded systems. Components in our model are cohesive collections of objects that publish contracts declaring the conditions under which they access other components. These contracts localize a component’s contextual synchronization dependencies in its interface. Moreover, the resulting systems permit strong guarantees of safety.

This paper reports a case study to validate the efficacy of our model on a realistic design problem: the component-based design of a multi-threaded web server. We first developed a bare-bones web server based on the Apache architecture and then subjected this design to three extension tasks. The study corroborates that our model enables a fine-grain component-based design of multi-threaded applications of realistic complexity, while guaranteeing freedom from certain synchronization errors.

Safe and Reliable Use of Concurrency in Multi-Threaded Shared-Memory Systems, R. E. Kurt Stirewalt, R. Behrends, and Laura K. Dillon, Proceedings of the 29th Annual IEEE/NASA on Software Engineering Workshop SEW '05, April 2005.

© IEEE, (2005). This is the author's version of the work. It is posted here by for your personal use. Not for redistribution. The definitive version was published in Proc. SEW’05, http://dx.doi.org/10.1109/SEW.2005.39.

Abstract. The safe and reliable use of concurrency in multi-threaded systems has emerged as a fundamental engineering concern. We recently developed a model of synchroniztion contracts to address this concern in programs written in object-oriented languages. Programs written using our model comprise modules that declare access requirements in module interfaces in lieu of using low-level synchronization primitives in module implementations. At run time, these contracts are negotiated to derive schedules that guarantee freedom from data races while avoiding a large class of deadlock situations.

Avoiding Serialization Vulnerabilities Through the Use of Synchronization Contracts, R. Behrends, R. E. K. Stirewalt, L. K. Dillon, Proc. ASE Work. Specification and Automated Processing of Security Requirements, Linz, Austria, September 2004.

Abstract:

Inference Graphs: A Computational Structure Supporting Generation of Customizable and Correct Analysis Components, Laura K. Dillon and R. E. Kurt Stirewalt, IEEE Transactions on Software Engineering, vol. 29, no. 2, February 2003, pp. 133-150.

© IEEE, (2003). This is the author's version of the work. It is posted here by permission of IEEE for your personal use. Not for redistribution. The definitive version was published in IEEE Trans. Software Engineering, http://dx.doi.org/10.1109/TSE.2003.1178052.

Abstract. Amalia is a generator framework for constructing analyzers for operationally defined formal notations. These generated analyzers are components that are designed for customization and integration into a larger environment. The customizability and efficiency of Amalia analyzers owe to a computational structure called an inference graph. This paper describes this structure, how inference graphs enable Amalia to generate analyzers for operational specifications, and how we build in assurance. On another level, this paper illustrates how to balance the need for assurance, which typically implies a formal proof obligation, against other design concerns, whose solutions leverage design techniques that are not (yet) accompanied by mature proof methods. We require Amalia-generated designs to be transparent with respect to the formal semantic models upon which they are based. Inference graphs are complex structures that incorporate many design optimizations. While not formally verifiable, their fidelity with respect to a formal operational semantics can be discharged by inspection.

Index Terms—Amalia, analysis software, engineering trade-offs, inference graphs, operational semantics, program transformations, proofs of correctness, transparent design.

Proof of correctness of a transparent design abstraction Laura K. Dillon and R. E. Kurt Stirewalt. Submitted. (A technical report provides details of the proofs in this paper.)

Abstract. Amalia is a generator framework for constructing analyzers for operationally defined formal notations. In performing an analysis, an Amalia-generated analyzer constructs and evaluates a network of collaborating objects, called an inference graph. The key result of this paper is a proof of correctness of inference graphs. Experience shows that it can be difficult to ``wrap one's mind'' around complex collaborations, such as those carried out by inference graphs. Moreover, many of the programming techniques (e.g, mixin classes and the visitor pattern) that are used in implementing inference graphs lack mature proof techniques. We therefore develop a formal model of inference graphs to use in the proof. This model is: (1) abstract enough to permit reasoning about the functional behavior of an inference graph and yet (2) not so abstract that its fidelity cannot be discharged by inspection. Such a high-fidelity model is said to be transparent. The transparent model of an inference graph aids understanding and enables us to structure the proof to conform to the collaborative nature of the graph.

Generation of Visitor Components that Implement Program Transformations R. E. Kurt Stirewalt and Laura K. Dillon. Proc. Symposium on Software Reuse, Toronto, May 2001.

© ACM, (2001). This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in SSR '01: Proceedings of the 2001 Symposium on Software Reusability, http://doi.acm.org/10.1145/375212.375258.

The visitor pattern is appealing to developers of program-analysis tools because it separates the design of the data structures that represent a program from the design of software that traverses these structures. Unfortunately, the visitor pattern is difficult to apply when the analysis involves transformation logic that involves multiple program fragments simultaneously. We encountered this problem in our work on the Amalia project and discovered a novel way to use multiple cooperating visitor objects to systematically implement such functions when they are specified via a set of transformation rules. This paper introduces our curried-visitor framework and illustrates how we applied it to implement a key component in the Amalia framework. We are working on a code generator that will automatically synthesize curried-visitor frameworks from a description of a program's abstract syntax and a set of pattern-matching transformation rules.

Keywords: Amalia, curried visitor framework, lightweight analysis components, program transformations, visitor pattern

A Component-Based Approach to Building Formal Analysis Tools R. E. Kurt Stirewalt and Laura K. Dillon. Proceedings of the 2001 International Conference on Software Engineering, Toronto, May 2001.

Abstract. Automatic-verification capability tends to be packaged into stand-alone tools, as opposed to components that are easily integrated into a larger software-development environment. Such packaging complicates integration because it involves translating internal representations into a form compatible with the stand-alone tool. By contrast, lightweight-analysis components package analysis capability in a form that does not involve such a translation. Borrowing ideas from GenVoca and object-oriented design patterns, we developed a domain model and an automatic-generation framework for lightweight-analysis components. The generated components operate directly over the internal form of a specification without requiring a change in representation. Moreover, the domain model identifies several ``useful subsets'' that can be used to customize analysis capability to a particular application. We validated this domain model by generating lightweight analyzers for temporal logic and the behavioral subset of Lotos.

Keywords: Component-based software engineering, environments: organization and integration principles, object-oriented technology, patterns and frameworks, reuse, formal analysis tools, layered design, artifactual representation change

Lightweight analysis of operational specifications using inference graphs, Laura K. Dillon and R. E. Kurt Stirewalt. Proceedings of the 2001 International Conference on Software Engineering, Toronto, May 2001.

Abstract. The Amalia framework generates lightweight components that automate the analysis of operational specifications and designs. A key concept is the step analyzer, which enables Amalia to automatically tailor high-level analyses, such as behavior simulation and model checking, to different specification languages and representations. A step analyzer uses a new abstraction, called an inference graph, for the analysis. It creates and evaluates an inference graph on-the-fly during a top-down traversal of a specification to deduce the specification's local behaviors (called steps). The nodes of an inference graph directly reify the rules in an operational semantics, enabling Amalia to automatically generate a step analyzer from an operational description of a notation's semantics. Inference graphs are a clean abstraction that can be formally defined. The paper provides a detailed, but informal, introduction to inference graphs. It uses example specifications written in Lotos for purposes of illustration.

Keywords: Testing, analysis, and verification, patterns and frameworks, formal methods, lightweight analysis components, operational specifications, automated software generators.

Analysis of a Scheduler for a CAD Framework. D. S. Keyes, L. K. Dillon, and M. J. Chung. Proceedings of the 1999 International Conference on Software Engineering, Los Angeles, May 1999, pp. 152-162

© ACM, (1999). This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in Proc. ICSE’99.

Abstract. This paper describes a case study in which a key component of a software system was modeled and analyzed to better understand a proposed algorithm prior to implementation. A Promela model of a linear scheduler for a CAD framework was developed. The Spin simulator was used to debug the model and, later, to illustrate how the algorithm works in different scenarios. Additionally, the Spin verifier was used to check various safety and liveness properties. The study revealed several deficiencies with the algorithm, as originally proposed. Subsequently, the modeling tools provided by Spin were used in devising solutions to the problems. Finally, the Promela model was modified and verified to be correct. The actual implementation of the scheduler involves a significant amount of message passing, multiple execution threads, and potentially huge data structures. By focusing on the interfaces between threads, restricting the system scope, and abstracting away details of data structures and irrelevant computations, a very simple model was obtained, which nevertheless provides an accurate representation of the communication between threads. The paper describes the steps that were abstracted and highlights the restrictions imposed on the model.

Analyzing Partially-Implemented Real-Time Systems. G. S. Avrunin, J. C. Corbett, and L. K. Dillon. IEEE Transactions on Software Engineering, vol. 24, no. 8, pp. 602-614, August 1998. (Revised and expanded version of a paper of the same title appearing in the Proceedings of the International Conference on Software Engineering, Boston, May 1997, 228-238.)

© IEEE, (1997). This is the author's version of the work. It is posted here for your personal use. Not for redistribution. The definitive version was published in IEEE Transactions on Software Engineering, http://dx.doi.org/10.1109/32.707696.

Abstract. Most analysis methods for real-time systems assume that all the components of the system are at roughly the same stage of development and can be expressed in a single notation, such as a specification or programming language. There are, however, many situations in which developers would benefit from tools that could analyze partially-implemented systems, those for which some components are given only as high-level specifications while others are fully implemented in a programming language. In this paper, we propose a method for analyzing such partially-implemented real-time systems. Here we consider real-time concurrent systems for which some components are implemented in Ada and some are partially specified using regular expressions and Graphical Interval Logic (GIL), a real-time temporal logic. We show how to construct models of the partially-implemented systems that account for such properties as run-time overhead and scheduling of processes, yet support tractable analysis of nontrivial programs. The approach can be fully automated, and we illustrate it by analyzing a small example.

Task Dependence and Termination in Ada, Laura K. Dillon, ACM Transactions on Software Engineering and Methodology, vol. 6, no. 1, pp. 80--110, January 1997.

© ACM, (1997). This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in ACM TOSEM, http://doi.acm.org/10.1145/237432.237459

Abstract. The paper analyzes the semantics of task dependence and termination in Ada. We use a contour model of Ada tasking in examining the implications of and possible motivation for the rules that determine when procedures and tasks terminate during execution of an Ada program. The termination rules prevent the data that belong to run-time instances of scope units from being deallocated prematurely, but they are unnecessarily conservative in this regard. For task instances that are created by invoking a storage allocator, we show that the conservative termination policy allows heap storage to be managed more efficiently than a less conservative policy. The paper also examines the manner in which the termination rules affect the synchronization of concurrent tasks. Master-slave and client-server applications are considered. We show that the rules for distributed termination of concurrent tasks guarantee that a task terminates only if it can no longer affect the outcome of an execution. The paper is meant to give programmers a better understanding of Ada tasking, and to help language designers assess the strengths and weaknesses of the termination model.

A Graphical Environment for Design of Concurrent Real-Time Systems, L. E. Moser, Y. S. Ramakrishna, G. Kutty, P. M. Melliar-Smith and L. K. Dillon, ACM Transactions on Software Engineering and Methodology, vol. 6, no. 1, pp. 31--79, January 1997.

Abstract. Concurrent real-time systems are among the most difficult systems to design be cause of the many possible interleavings of events and because of the timing requirements that must be satisfied. We have developed a graphical environment based on Real-Time Graphical Interval Logic (RTGIL) for specifying and reasoning about the designs of concurrent real-time systems. Specifications in the logic have an intuitive graphical representation that resembles the timing diagrams drawn by software and hardware engineers, with real-time constraints that bound the durations of intervals. The syntax-directed editor of the RTGIL environment enables the user to compose and edit graphical formulas on a workstation display; the automated theorem prover mechanically checks the validity of proofs in the logic; and the database and proof manager tracks proof dependencies and allows formulas to be stored and retrieved. This paper describes the logic, methodology, and tools that comprise the prototype RTGIL environment and illustrates the use of the environment with an example application.

Generating Oracles from Your Favorite Temporal Logic Specifications, Laura K. Dillon and Y. S. Ramakrishna, Proc. 4th ACM SIGSOFT Symp. Foundations of Software Engineering, San Francisco, pp. 106-117, October 1996.

Abstract. This paper describes a generic tableau algorithm, which is the basis for a general customizable method for producing oracles from temporal logic specifications. A generic argument gives semantic rules with which to build the semantic tableau for a specification. Parameterizing the tableau algorithm by semantic rules permits it to easily accommodate a variety of temporal operators and provides a clean mechanism for fine-tuning the algorithm to produce efficient oracles.

The paper develops conditions to ensure that a set of rules results in a correct tableau procedure. It gives sample rules for a variety of linear-time temporal operators and shows how rules are tailored to reduce the size of an oracle.

Interval Logics and Their Decision Procedures, Part I: An Interval Logic, Y. S. Ramakrishna, P. M. Melliar-Smith, L. E. Moser, L. K. Dillon, and G. Kutty, Theoretical Computer Science, vol. 166, nos. 1-2, pp. 1-47, October 1996.

Abstract. We present an interval logic, called Future Interval Logic (FIL), for the specification and verification of concurrent systems. Interval logics allow reasoning to be carried out at the level of time intervals, rather than instants. However, unlike some other interval logics, the primitive objects in our semantic model for FIL are not intervals, but instants. An interval is formed by identifying its end-points, which are instants satisfying given properties. The logic has an intuitive graphical representation, resembling the back-of-the-envelope timing diagrams that designers often draw to reason about concurrent interacting systems. The logic is designed to be insensitive to finite stuttering (a property that facilitates refinement-based multi-level correctness proofs), and is exactly as expressive as the fragment of Propositional Temporal Logic with 'until' but not 'next'. As the main result of this paper, we show that FIL is elementarily decidable by reduction to the emptiness problem for Buchi Automata. For most other interval logics the decision problem is at best non-elementary and often undecidable. We condiser an extension of FIL with past operators and show that this extension leads to non-elementariness. In a companion paper, we extend the logic to real-time and investigate the decision problem for that extension.

Interval Logics and Their Decision Procedures, Part II: A Real-Time Interval Logic, Y. S. Ramakrishna, P. M. Melliar-Smith, L. E. Moser, L. K. Dillon, and G. Kutty, Theoretical Computer Science, vol. 170, nos. 1-2, pp. 1-46, December 1996.

Abstract. In a companion paper, we presented an interval logic, and showed that it is elementarily decidable. In this paper we extend the logic to allow reasoning about real-time properties of concurrent systems; we call this logic Real-Time Future Interval Logic (RTFIL). We model time by the real numbers, and allow our syntax to state the bounds on the duration of an interval. RTFIL possesses the "real-time interpolation property," which appears to be the natural quantitative counterpart of invariance under finite stuttering. As the main result of this paper, we show that RTFIL is decidable; the decision algorithm is slightly more expensive than for the untimed logic. Our decidability proof is based on the reduction of the satisfiability problem for the logic to the emptiness problem for timed Buchi automata. The latter problem was shown decidable by Alur and Dill in a landmark paper, in which this real-time extension of w-automata was introduced. Finally, we consider an extension of the logic that allows an interval to be constructed by means of "real-time offsets," and show that even this simple extension renders the logic highly undecidable.

Axiomatizations of Interval Logics (with G. Kutty, P. M. Melliar-Smith, L. E. Moser and Y. S. Ramakrishna), Fundamenta Informaticae, vol. 24, no. 4, pp. 313-331, December 1995.

Abstract.

Automated Deduction in a Graphical Temporal Logic (with G. Kutty, P. M. Melliar-Smith, L. E. Moser and Y. S. Ramakrishna), Journal of Applied Non-Classical Logics, vol. 6, no. 1/1996, pp. 29-47.

Abstract. Real-time graphical interval logic is a modal logic for reasoning about time in which the basic modality is the interval. The logic differs from other logics in that it has a natural intuitive graphical representation that resembles the timing diagrams drawn by system designers. We have developed an automated deduction system for the logic, which includes a theorem prover and a user interface. The theorem prover checks the validity of proofs in the logic and produces counterexamples to invalid proofs. The user interface includes a graphical editor that enables the user to create graphical formulas on a workstation display, and a database and proof manager that tracks proof dependencies and allows graphical formulas to be stored and retrieved. In this paper we describe the logic, the automated deduction system, and an application to robotics.

Oracles for Checking Temporal Properties of Concurrent Systems (with Q. Yu), Proceedings of the 2nd ACM SIGSOFT Symposium on Foundations of Software Engineering (SIGSOFT'94). Proceedings published as Software Engineering Notes, vol. 19, no. 5, pp. 140-153 December 1994.

© ACM, (1994). This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in IEEE Transactions on Software Engineering, http://doi.acm.org/10.1145/193173.195401 .

Abstract. Verifying that test executions are correct is a crucial step in the testing process. Unfortunately, it can be a very arduous and error-prone step, especially when testing a concurrent system. System developers can therefore benefit from oracles automating the verification of test executions.

This paper examines the use of Graphical Interval Logic (GIL) for specifying temporal properties of concurrent systems and describes a method for constructing oracles from GIL specifications. The visually intuitive representation of GIL specifications makes them easier to develop and to understand than specifications written in more traditional temporal logics. Additionally, when a test execution violates a GIL specification, the associated oracle provides information about a fault. This information can be displayed visually, together with the execution, to help the system developer see where in the execution a fault was detected and the nature of the fault.

Automated Derivation of Time Bounds in Uniprocessor Concurrent Systems (with G. Avrunin, J. Corbett, and J. Wileden), IEEE Transactions on Software Engineering, vol. 20, no. 9, pp. 708-719, September 1994.

© ACM, (2001). This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in SSR '01: Proceedings of the 2001 symposium on Software reusability, http://dx.doi.org/10.1109/32.317429.

Abstract. The successful development of complex real-time systems depends on analysis techniques that can accurately assess the timing properties of those systems. This paper describes a technique for deriving upper and lower bounds on the time that can elapse between two given events in an execution of a concurrent software system running on a single processor under arbitrary scheduling. The technique involves generating linear inequalities expressing conditions that must be satisfied by all executions of such a system and using integer programming methods to find appropriate solutions to the inequalities. The technique does not require construction of the state space of the system and its feasibility has been demonstrated by using an extended version of the constrained expression toolset to analyze the timing properties of some concurrent systems with very large state spaces.

First Order Future Interval Logic (with G. Kutty, P. M. Melliar-Smith, L. E. Moser and Y. S. Ramakrishna), Proceedings of the First International Conference on Temporal Logic, LNAI #827, Bonn, Germany, pp. 195-209, July 11-14 1994.

Abstract.

A Graphical Interval Logic for Specifying Concurrent Systems (with G. Kutty, P. M. Melliar-Smith, L. E. Moser and Y. S. Ramakrishna), ACM Transactions on Software Engineering and Methodology, vol. 3, no. 2, pp. 131-165, April 1994.

© ACM, (1994). This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in ACM TOSEM, http://doi.acm.org/10.1145/192218.192226

Abstract. The paper describes a graphical interval logic that is the foundation of a toolset supporting formal specification and verification of concurrent software systems. Experience has shown that most software engineers find standard temporal logics difficult to understand and to use. The objective of this work is to enable software engineers to specify and reason about temporal properties of concurrent systems more easily by providing them with a logic that has an intuitive graphical representation and with tools that support its use. To illustrate the use of the graphical logic, the paper provides some specifications for an elevator system and proves several properties of the specifications. The paper also describes the toolset and the implementation.

Visual Specifications for Temporal Reasoning (with G. Kutty, P. M. Melliar-Smith, L. E. Moser and Y. S. Ramakrishna), Journal of Visual Languages and Computing, vol. 5, no. 1, pp. 61-81, March 1994.

Abstract. Graphical Interval Logic (GIL) is a visual temporal logic in which formulas resemble the informal timing diagrams familiar to system designers and software engineers. It provides an intuitive and natural visual notation in which to express specifications for concurrent systems and retains the benefits of a formal notation. A visual editor permits GIL specifications to be easily constructed, and to be stored in and retrieved from files. The editor interfaces with a proof checker and model generator, which permit verification of temporal inferences. The paper shows how graphical specifications are created and used to reason about temporal properties of systems. It shows how pictures that formalize temporal arguments enhance understanding and help motivate successful proof strategies.

Really Visual Temporal Reasoning (with G. Kutty, P. M. Melliar-Smith, L. E. Moser and Y. S. Ramakrishna), Proceedings of the Fourth IEEE Real-Time Systems Symposium, pp. 262-273, Raleigh-Durham, NC, December 1993.

Abstract. Real-Time Future Interval Logic (RTFIL) is a visual logic with formulae that resemble timing diagrams. It is a dense real-time temporal logic that is based on two simple temporal primitives: interval modalities for the purely qualitative part and duration predicates for the quantitative part. In this paper we present the logic, and illustrate its use in specifying the railroad crossing example and proving some of its properties. The logic in its propositional form is decidable by reduction to the emptiness problem of Timed Buchi Automata. A theorem prover, based on this decision procedure, has been implemented as part of a graphical proof environment. The proofs of the railroad crossing example have been verified using this theorem prover. The combination of an automated theorem prover and a graphical specification language greatly facilitate the task of verifying real-time proofs. This convenience apart, RTFIL is invariant under real-time stuttering and does not admit instantaneous states. These properties facilitate proof methods based on abstraction and refinement.

A Visual Execution Model for Ada Tasking, ACM Transactions on Software Engineering and Methodology, vol. 2, no. 4, pp. 311-345, November 1993.

© ACM, (1993). This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in ACM TOSEM, http://doi.acm.org/10.1145/158431.158432 .

Abstract. A visual execution model for Ada tasking can help programmers attain a deeper understanding of the tasking semantics. It can illustrate subtleties in semantic definitions that are not apparent in natural language descriptions of Ada tasking, as well as the consequences of choices made in the language design.

We describe a contour model of Ada tasking that depicts asynchronous tasks (threads of control), relationships between the environments in which tasks execute, and the manner in which tasks interact. The use of this high-level execution model makes it possible to see what happens during execution of a program. The paper provides an introduction to the contour model of Ada tasking and demonstrates its use.

Laura K. Dillon <dillon@cs.ucsb.edu>

Last modified: Thu Aug 3 17:40:40 EDT 2006

Selected Publications of Laura K. Dillon

Selected Publications of
Laura K. Dillon