Automatic Generation of Inequality Systems for Constrained Expression Analysis
George S. Avrunin, Ugo A. Buy, James C. Corbett · 1990
This report describes a prototype tool for automating the generation of systems of inequalities, and for aiding in the interpretation of the solutions of such systems, in the analysis of constrained expressions. The constrained expression approach to the analysis of concurrent and distributed software systems is described in [4, 5]; more detailed descriptions of the use of inequalities in such analysis are given in [2, 5, 6]. This prototype implements a piece of a toolset supporting automated analysis of distributed system designs written in the CEDL design language [11], which is based on Ada. The structure of the toolset and its application are described briefly in the next section and in more detail in [4]. Detailed discussions of the other components of the toolset are given in [1, 7, 9, 12]. This document describes version 2.0 of the prototype, whose implementation has been completed recently. Version 2.0 of the prototype extends significantly an earlier version, described in [3], and incorporates algorithms and some portions of code from that version. A number of major areas have been changed. One such change is the added capability to generate inequalities from deterministic finite-state automata (DFAs) and a hybrid form we call regular expression deterministic finite-state automata (REDFAs) in addition to regular expressions. In some cases, these automata are significantly more compact representations of event sequences than their equivalent regular expressions and thus produce much smaller inequality systems. Also, if a task expression has been run through the constraint eliminator, and thus converted to a DFA or an REDFA, no time must then be spent converting it back to a regular expression.