How does Quasar proceed ?
Quasar is an automatic concurrent program analysis tool based on this promising method that uses the application source code for generating and validating a semantic model.
Quasar follows a four step process :
Automatic extraction of the source code which is related to the property to verify. The aim of this step is to remove those parts of the source code which are not related to the investigated property. This contributes to generate a model which is smaller than the one corresponding to the whole program, but which has the same behavior according to the investigated property. This smaller model will be easier to analyze in the next steps. This first step is called slicing.
Translation of the simplified program into a formal model. The target formalism used is colored Petri nets because their analysis may combine several techniques that are supported by experienced tools and that we continue to develop successfully. For translating an Ada program into a Petri net we use patterns. Each element of the Ada language has a corresponding pattern (or sub-net). These sub-nets allow a hierarchical construction since meta-nets can be used to abstract other (list of) sub-net(s). For example, the sub-net of the loop statement contains a meta-net abstracting the statements of the loop. We produce The final net corresponding to the whole (simplified) program is produced using two basic constructors : the substitution (that substitutes a meta-net by a concrete sub-net) and the composition (that merges two different sub-nets into an unique one).
Analysis of the model by combining structural techniques (like Petri nets reductions) and finite state verification methods (like temporal logic formula verification). The efficiency of this combination, added to the gain obtained by the slicing step, allows to analyze complex and relatively large programs.
Construction of a report. When the target property is not verified, the state in which the application is faulty is displayed and a report indicates the sequence of program actions that ends by invalidating the property.
last update : 20/10/2005