Abstract One class of program defects results from illegal sequences of otherwise legal operations in software implementations. Explicit statement of sequencing constraints, however, is not a common activity when specifying software even when using formal specification methods. This paper shows that constraints on program execution sequences can be derived directly from algebraic specifications. Results include heuristic methods for generating sequencing constraints and a generalization of these methods into automatable rules. The heuristics can be integrated into a specification methodology such as Larch. Engineers can use the generated sequencing constraints to detect sequencing defects in software even before dynamic testing begins. The method can be used to increase the reliability of software that is specified using algebraic methods.

One class of program defect results from illegal sequences of otherwise legal operations in software implementations. Expressions that specify the correct sequences can be written in the Cecil sequencing constraint language. Programs can then be checked at compile time by the Cesar analysis system. Explicit statement of sequencing constraints, however, is not a common activity when specifying software even when using formal specification methods. In this paper, we describe methods to derive constraints on program execution sequences from algebraic specifications. We provide heuristic methods for generating these constraints from the specifications and generalize the methods into automatable rules. Using these generated constraints, we can then detect sequencing defects in software before dynamic testing begins.

As software products evolve, regression testing is a necessary part of the development process. We present methods to automate and analyze change tracking for requirements and test cases so we may partially automate the process of revising the regression test suite for the modified software, and eliminate the necessity to rerun test cases that are unaffected by the modifications.>

This paper describes a system that automatically performs static interprocedural sequencing analysis from programmable constraint specifications. We describe the algorithms used for interprocedural analysis, relate the problems arising from the analysis of real-world programs, and show how these difficulties were overcome. Finally, we sketch the architecture of our prototype analysis system (called Cesar) and describe our experiences to date with its use, citing performance and error detection characteristics.

A flexible and general mechanism for specifying problems relating to the sequencing of events and mechanically translating them into dataflow analysis algorithms capable of solving those problems is presented. Dataflow analysis has been used for quite some time in compiler code optimization. Most static analyzers have been custom-built to search for fixed and often quite limited classes of dataflow conditions. It is shown that the range of sequences for which it is interesting and worthwhile to search in actually quite broad and diverse. A formalism for specifying this diversity of conditions is created. It is shown that these conditions can be modeled essentially as dataflow analysis problems for which effective solutions are known. It is also shown how these solutions can be exploited to serve as the basis for mechanical creation of analyzers for these conditions.>