Abstract In this paper, we present a method to generate abstractions for model checking concurrent systems. A program using a defined syntax and semantics, first describes the concurrent system that can be infinite. This program is abstracted using the framework of abstract interpretation where an abstract function will be given. This abstract program is demonstrated to be an accurate approximation of the original program that may contain spurious behaviours. These spurious behaviours will be identified and removed using a new defined abstraction framework based on the restrictions. The new produced abstract program is an exact approximation of the original program.

References

[1] Dwyer M., Clarke L., Cobleigh J., and Naumovich G., Flow Analysis for Verifying Properties of Concurrent Software Systems, ACM Transactions on Software Engineering and Methodology , vol. 13, pp. 359-430, 2004.

[2] Siegel S., Mironova A., Avrunin G., and Clarke L., Using Model Checking with Symbolic Execution to Verify Parallel Numerical Programs, in Proceedings of the International Symposium on Software Testing and Analysis , pp. 157-168, 2006.

[3] Peled D. and Qu H., Enforcing Concurrent Temporal Behaviors, International Journal of Foundations of Computer Science , vol. 17, pp. 743-762, 2006.

[4] Ostrovsky K., On Modelling and Analysing Concurrent Systems , PhD Dissertation, Computer Science and Electronic Engineering, Chalmers University of Technology, Sweden, 2005.

[5] Clarke E., Grumberg O., and Peled D., Model Checking , The MIT Press, 2000.

[6] Cousot P., Abstract Interpretation, ACM Computing Surveys , vol. 28, pp. 205-212, 1996.

[7] Dams D., Gerth R., and Grumberg O., Abstract Interpretation of Reactive Systems, ACM Transactions on Programming Languages and Systems , vol. 19, pp. 115-132, 1997.

[8] Chouali S., Julliand J., Masson P., and Bellegarde F., PLTL Partitionned Model- Checking for Reactive Systems Under Fairness Assumptions, ACM Transactions on Embedded , ,think think e, ,think eat e Generating Exact Approximations to Model Check Concurrent Systems 145 Computing Systems , vol. 4, no. 2, pp. 267-301, 2005.

[9] Clarke E., Grumberg O., Jha S., Lu Y., and Veith H., Counterexample-Guided Abstraction Refinement for Symbolic Model Checking, Journal of the ACM , vol. 50, no. 5, pp. 752-794, 2003.

[10] Clarke E., Grumberg O., and Long D., Model Checking and Abstraction, ACM Transactions on Programming Languages and Systems , vol. 16, pp. 81-112, 1994.

[11] Clarke E., Emerson E., and Sistla A., Automatic Verification of Finite-state Concurrent Systems Using Temporal Logic Specifications, ACM Transactions on Programming Languages and Systems , vol. 8, pp. 54-66, 1986.

[12] Emerson E. and Lei C., Efficient Model Checking in Fragments of the Prepositional m - Calculus, in Proceedings of the First Annual Symposium of Logic in Computer Science , 1986.

[13] Bryant R., Graph-Based Algorithms for Boolean Function Manipulation, IEEE Transactions on Computers , vol. 35, pp. 78-105, 1986.

[14] Grumberg O. and Long D., "Model Checking and Modular Verification," Lecture Notes in Computer Science (LNCS), Springer, 1991.

[15] Bourahla M. and Benmohamed M., Predicate Abstraction and Refinement for Model Checking VHDL State Machines, Electronic Notes in Theoretical Computer Science , Elsevier Science, vol. 66, pp. 3-17, 2002.

[16] Bourahla M. and Benmohamed M., Abstract Model Checking Infinite State Systems, in ACS/IEEE International Conference on Computer Systems and Applications , pp. 83, 2003.

[17] Bourahla M. and Benmohamed M., Verification of Real-Time Systems by Abstraction of Time Constraints, in Proceedings of the 17 th International Symposium on Parallel and Distributed Processing (IPDPS 2003), IEEE Computer Society, 2003.

[18] McMillan K., Symbolic Model Checking , Kluwer Academic Publishers, 1993.

[19] Tzoref R. and Grumberg O., Automatic Refinement and Vacuity Detection for Symbolic Trajectory Evaluation, in Proceedings of the International Conference on Computer Aided Verification (CAV'06) , 2006.

[20] Grumberg O., Lerda F., Strichman O., and Theobald M., Underapproximation-Widening for Multi-Process Systems, in Proceedings of the 32 nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'05) , 2005.

[21] Shoham S. and Grumberg O., Monotonic Abstraction-Refinement for CTL, in Proceedings of the Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'04) , 2004.

[22] Rabinovitz I. and Grumberg O., Bounded Model Checking of Concurrent Programs, in Proceedings of the International Conference on Computer Aided Verification (CAV'05) , 2005. Mustapha Bourahla has a PhD degree in computer science from the University of Biskra, Algeria in 2007 and has the Master degree in computer science from the university of Montreal, Canada in 1989. He was a member of the VHDL group at Bell- Northern Research, Ottawa, Canada during 1989-1993. He worked for Bell Canada for one year. Currently, he is teacher-researcher at the University of Biskra, Algeria. He has publications in the domains of VLSI and formal methods. His current research interests are in formal methods, especially model checking critical systems. He is a member of a research group working in the domains of VLSI and formal methods at the University of Biskra, Algeria.