George S. Avrunin, James C. Corbett, and Laura K. Dillon. Analyzing partially-implemented real-time systems. IEEE Trans. Softw. Eng., 24(8):602–614, August 1998. (This is a revised and expanded version of a paper of the same title appearing in the Proceedings of the International Conference on Software Engineering, 1997.). [ DOI | .pdf ]
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.
George S. Avrunin, James C. Corbett, and Laura K. Dillon. Analyzing partially-implemented real-time systems. In ICSE '97: Proceedings of the 19th International Conference on Software Engineering, pages 228–238, New York, NY, USA, 1997. ACM. [ DOI | .pdf ]
George S. Avrunin. Concurrent and real-time systems. In Quality-Enhancing Software Technologies. Microelectronics and Computer Technology Corporation (MCC), 1996.
George S. Avrunin, James C. Corbett, Laura K. Dillon, and Jack C. Wileden. Automated derivation of time bounds in uniprocessor concurrent systems. IEEE Trans. Softw. Eng., 20(9):708–719, September 1994. [ DOI | .pdf ]
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.
James C. Corbett and George S. Avrunin. A practical technique for bounding the time between events in concurrent real-time systems. In Thomas Ostrand and Elaine Weyuker, editors, Proceedings of the 1993 International Symposium on Software Testing and Analysis (ISSTA), pages 110–116, Cambridge, MA, June 1993. ACM Press. [ DOI | .pdf ]
Showing that concurrent systems satisfy timing constraints on their behavior is difficult, but may be essential for critical applications. Most methods are based on some form of reachability analysis and require construction of a state space of size that is, in general, exponential in the number of components in the concurrent system. In an earlier paper with L. K. Dillon and J. C. Wileden, we described a technique for finding bounds on the time between events without enumerating the state space, but the technique applies chiefly to the case of logically concurrent systems executing on a uniprocessor, in which events do not overlap in time. In this paper, we extend that technique to obtain upper bounds on the time between events in maximally parallel concurrent systems. Our method does not require construction of the state space and the results of preliminary experiments show that, for at least some systems with large state spaces, it is quite tractable. We also briefly describe the application of our method to the case in which there are multiple processors, but several processes run on each processor.
George S. Avrunin. Sharpening bounds on the time between events in maximally parallel systems. Technical Report 92-69, Department of Computer Science, University of Massachusetts at Amherst, 1992.
A recent paper describes a method for obtaining 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. Corbett has extended this approach to obtain upper bounds on the time between events in executions of multi-processor concurrent systems in which each process proceeds unless forced to wait to communicate with another, the case of maximal parallelism, and processes communicate by synchronous message passing. Corbett's method does not strictly enforce the maximal parallelism assumption, however, and may thus give poor (though valid) bounds in some cases. In this paper, I show how to modify Corbett's method to obtain sharper bounds.
George S. Avrunin and Jack C. Wileden. Improvements in automated analysis of concurrent and real-time software. In André M. van Tilborg and Gary M. Koob, editors, Foundations of Real-Time Computing: Formal Specifications and Methods, chapter 8, pages 195–215. Kluwer Academic Publishers, 1991.
George S. Avrunin, Laura K. Dillon, and Jack C. Wileden. Constrained expression analysis of real-time systems. Technical Report 89-50, Department of Computer and Information Science, University of Massachusetts, 1989.
This file was generated by bibtex2html 1.99.
![[Back]](/icons/back.gif){kind=icon}
Back to George Avrunin's home page