Basic papers :
2006A new approach for concurrent program slicing. In International Conference on Formal Methods for Networked and Distributed Systems (FORTE'06), paper accepted. Paris, France, sep. 2006.
Abstract : Regarding the progress made in model analysis, more complex models, and consequently more complex programs can now be analyzed. However, this remains a difficult task in particular for concurrent programs which induce a lot of combinatory. Another way to reduce this complexity is to use program decomposition. Program decomposition technics extract a part of a given program while preserving the behavior of the original program w.r.t. a specified property.
Quasar analyzes concurrent Ada programs, using program slicing as decomposition technic. The program slicer is built using the ASIS tools, that provides syntactic and semantic informations on an Ada source code. These informations can be considered as the ``semantic and syntactic graph'' mapping an Ada program. This allows to save building the graphs used by traditional program slicing technics and thus to design a simpler and more evolutive algorithm.
This paper presents Yasnost, the program slicer used by Quasar, describes the method used to slice concurrent Ada programs and illustrates with two significant examples how concurrent programs analysis can take advantage of program slicing for reducing the analyzed program complexity.
Dynamic tasks verification with Quasar. In International Conference on Reliable Software Technologies, Ada-Europe (Ada-Europe'05), LNCS vol. 3555, p.91-104, Springer-Verlag 2005, ISBN: 3-540-26286-5. York, United Kingdom, jun. 2005.
Abstract : The inclusion of dynamic tasks modelisation in Quasar, a tool for automatic analysis of concurrent programs, extends its applicative usefulness. However this extension leads to large size models whose processing has to face combinatory explosion of modelling states.
This paper presents briefly Ada dynamic tasks semantic and dependences and then it explains the choice of an efficient generic modelling pattern. This implies to consider the naming, the hierarchy, the master retrieval, the termination of dynamic tasks and their synchronization dependences successively. The adequacy of both this modelling and the Quasar techniques is highlighted by the analysis of two non-trivial Ada programs. The large reduction factor between the initial and final state numbers of these program models shows that the state explosion can be limited, making automatic validation of dynamic concurrent programs feasible.
Concurrent Ada program slicing for source code understanding and formal analysis CEDRIC Technical Report No 708, 2005.
Abstract : Quasar is a tool for validating formally properties on concurrent programs. The main steps followed by Quasar to carry out validation can be viewed themselves as independent tools : the program slicer, the model builder and the model checker.
The program slicer removes from the source code the parts not related to concurrency or to the property to verify. The model builder translates a source code into a formal model. Finally the model checker verify the property on the model. This report briefly describes Quasar and program slicing, and gives the algorithm used by Quasar to slice concurrent Ada programs using the ASIS tools.
Extending Quasar with dynamic tasks computation CEDRIC Technical Report No 695, 2005.
Abstract : The inclusion of dynamic tasks modelisation in Quasar, a tool for automatic analysis of concurrent programs, extends its applicative usefulness. However this extension leads to large size models whose processing has to face combinatory explosion of modeling states. This article is an extension of the paper \'Dynamic tasks verification with Quasar\' accepted for publication in the 10th International Conference on Reliable Software Technologies Ada-Europe 2005. It gives some insight into the impact of the way used to name dynamic task in term of state space size by comparing different solutions on several exemples.
Slicing concurrent programs using the Quasar tool In International Conference "Software and Systems Engineering and their Applications" (ICSSEA'04). Paris, France, dec. 2004.
Abstract : Systems requiring a high degree of reliability and safety have to support concurrents process. However, the indeterminism related to concurrency is a barrier to their use. Quasar is a tool designed to solve this problem. Quasar proves, in a formal way, properties on concurrent programs using a formal model, obtained by automatic translation of the source code. However, to avoid the modeling of the complete source code, we eliminate from it the statements that don\'t have any effect on the property to validate. This is called program slicing. It is the first step of the process followed by Quasar to validate a property. Slicing can be used independently because the slice obtained by this method has the same behavior as the original source code from the point of view of the studied property. In this article, we give a short outline of Quasar as well as general principles of program slicing and its use. Then we present the techniques used by Quasar to carry it out.
Verifying Linear Time Temporal Logic properties of concurrent Ada programs with Quasar. In ACM Annual International Conference on Ada (SIGAda'03), p. 17-24, ISBN:1-58113-476-2. San Diego, USA, dec. 2003.
Abstract : In this paper we present an original and useful way for specifying and verifying temporal properties of concurrent programs with our tool named Quasar. Quasar is based on ASIS and uses formal methods (model checking). Properties that can be checked are either general, like deadlock or fairness, or more context specific, referring to tasks states or to value of variables; properties are then expressed in temporal logic. In order to simplify the expression of these properties, we define some templates that can be instantiated with specific items of the programs. We demonstrate the usefulness of these templates by verifying subtle variations of the Peterson algorithm. Thus, although Quasar uses up-to-date formal methods it remains accessible to a large class of practitioners.
Quasar : a new tool for analyzing concurrent programs. In International Conference on Reliable Software Technologies, Ada-Europe (Ada-Europe'03), LNCS vol. 2655, p.166-181, Springer-Verlag 2003, ISBN: 3-540-40376-0. Toulouse, France, jun. 2003.
Abstract : Concurrency introduces a high degree of combinatory which may be the source of subtle mistakes. We present a new tool, Quasar, which is based on ASIS and which uses fully the concept of patterns. The analysis of a concurrent Ada program by our tool proceeds in four steps : automatic extraction of the concurrent part of the program; translation of the simplified program into a formal model using predefined patterns that are combined by substitution and merging constructors; analysis of the model both by structural techniques and model-checking techniques; reporting dead-lock or starvation results. We demonstrate the usefulness of Quasar by analyzing several variations of a non trivial concurrent program.
You can also find some related materials to this publication :
last update : 30/06/2005