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 deadlock or starvation results. We demonstrate the usefulness of Quasar by analyzing several variations of a non trivial concurrent program.
References in zbMATH (referenced in 3 articles , 1 standard article )
Showing results 1 to 3 of 3.
- Evangelista, Sami; Pradat-Peyre, Jean-François: Memory efficient state space storage in explicit software model checking (2005)
- Evangelista, S.; Haddad, S.; Pradat-Peyre, J.-F.: Syntactical colored Petri nets reductions (2005)
- Evangelista, Sami; Kaiser, Claude; Pradat-Peyre, Jean-François; Rousseau, Pierre: Quasar: A new tool for concurrent Ada programs analysis (2003)