|
 
|
[EKP03a] Verifying Linear Time Temporal Logic Properties of Concurrent Ada Programs with Quasar
Revue Internationale avec comité de lecture : Journal ACM Ada Letters, vol. 24(1), pp. 17-24, 2003
motcle:
Résumé:
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.
BibTeX
| @article { | |||
| EKP03a, | |||
| title | = | "{Verifying Linear Time Temporal Logic Properties of Concurrent Ada Programs with Quasar}", | |
| author | = | "S. Evangelista and C. Kaiser and J. Pradat-Peyre and P. Rousseau", | |
| journal | = | "ACM Ada Letters", | |
| year | = | 2003, | |
| volume | = | 24, | |
| number | = | 1, | |
| pages | = | "17-24", | |
| } | |||
