FLAVERS constructs annotated control flow graphs for the tasks of the program from the Ada code, and adds edges connecting nodes in different tasks based on the possible interleavings of events from the tasks to build a Trace Flow Graph. Paths through this graph then represent possible sequences of events, represented by the annotations, that could be seen on executions of the program. FLAVERS uses a regular expression-based formalism to represent the property to be checked, and propagates states of an FSA representing the property through the Trace Flow Graph to check whether the property holds. FLAVERS provides a mechanism for adding information, in the form of additional FSAs called feasibility constraints, to eliminate infeasible paths and increase the precision of the analysis.
The Ada source code must be significantly modified to allow analysis by FLAVERS. First, because annotations must be placed on a control flow graph node that corresponds to a block of code and a single call or accept statement in Ada may be executed with different values of the parameters, it is not possible to insert an annotation that represents a rendezvous with a particular set of parameter values. It is therefore necessary to modify the Ada code to create separate calls and entries for each possible set of parameter values that could be passed in a given rendezvous. Second, because FLAVERS cannot represent the use of a variable as an index into an array or directly handle situations where the value of one variable is set to the current value of another variable, it is necessary to unroll all the loops in which arrays are searched and updated, and to add explicit case statements to handle the updating of the arrays. The modified Ada code follows.