Question

Discuss solution domains, forward vs. backward,GEN,MAY,MUST, KILL as it relates to static verification.

Answer 1

The solution domain defines the abstract environment where the solution is developed. The solution space consists of software entities in the implementation of the solution.

In solution domain engineers use their ingenuity to solve problems. The primary characteristic that differentiates the solution domain from the problem domain is that, invariably, requirements engineering in the solution domain starts with a given set of requirements. In the problem domain requirements engineering starts with a vague objective or wish list. At each level there is modelling and analysis done to first understand the input requirements and secondly to provide a sound basis for deriving the requirements for the next level down. The number of levels of design is dictated by the nature of the application domain and the degree of innovation involved in the development.

At every level in the solution domain, engineers must make decisions that move towards the final solution. Each of these decisions, by their very nature reduces the available design space; that is, they preclude certain design options, but it is impossible to make progress in the absence of decisions.

The first level of system development in the solution domain is to transform the stakeholder/customer requirements into a set of system requirements. These must define what the system must do in order to solve the problems posed by the stakeholder/customer requirements. The next step after defining the system requirements is to create an architectural design...

In respect to a given problem (or set of problems), the solution domain (or solution space) covers all aspects of the solution product, including:

1. The process by which the solution is arrived at;
2. The environment in which it is constructed;
3. The design, construction, testing, operation, and functions of the solution product itself.

Data Flow Analysis is a type of static analysis/verification. The goal of static analysis/verification is to find out program behavior at compile-time, before ever running the program. Data Flow Analysis/verification typically operates over a Control-Flow Graph (CFG), a graphical representation of a program.

Direction in data flow analysis/verification:

• Forward: For each node and edge,compute information about past behavior,
• Backward:For each node and edge,compute information about future behavior.

Consider an arbitrary program point p. In a forward analysis, we are reasoning about facts up to p, considering only the predecessors of the node at p. In a backward analysis, we are reasoning about facts from p onward, considering only the successors.

Transfer function:

• Join: Specifies how information from adjacent nodes/edges is propagated.

1. MAY: Union of adjacent edges
2. MUST: Intersection of adjacent edges

• GEN: Specifies which specific solution are generated at the node/edge
• KILL: Specifies which specific solution are removed at that node/edge

In a MAY analysis, we care about the facts that may be true at p. That is, they are true for some path up to or from p, depending on the direction of the analysis. In a MUST analysis, we care about the facts that must be true at p. That is, they are true for every path up to or from p. This manifests when we reach a join point in our program. A join point is when multiple paths of a program come together in our CFG. At these join points, we will either take the union (for MAY) or intersection (for MUST) of sets of facts.

We generate facts when we have new information at a program point, and we KILL facts when that program point invalidates other information. We call these sets GEN and KILL. A variable is only live if it's used, so using a variable in an expression generates information. A variable is only live if it's used before it is overwritten, so assigning to the variable kills information.

From this emerges a generic algorithm:

If we are moving forward, we have the following:

          In(s) = /\s' in pred(s) Out(s')
         Out(s) = Gen(s) union (In(s) \ Kill(s))

If we are moving backward, we instead have the following:

       Out(s) = /\s' in succ(s) In(s')
        In(s) = Gen(s) union (Out(s) \ Kill(s))

Here, /\ refers to "meet," which is union for may analyses and intersection for must analyses.

when we move forward, we get our input by taking the union or intersection of the outputs of all of the predecessors, and we get our output by reasoning locally about the facts generated and killed at that point. When we move backward, we get our output by taking the union or intersection of all the inputs of all of the successors, and we get our input by reasoning locally about our facts. The algorithm is executed until all facts converge, that is, until they don't change anymore.