Abstractions with Strong Preservation of Concurrent Systems


(*) Corresponding author


Authors' affiliations


DOI's assignment:
the author of the article can submit here a request for assignment of a DOI number to this resource!
Cost of the service: euros 10,00 (for a DOI)

Abstract


In this paper, we present a method to generate strongly preserving abstractions for model checking concurrent systems. The concurrent system which can be infinite, is first described by a program using a defined syntax and semantics. 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 which may contain spurious behaviors. These spurious behaviors 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.
Copyright © 2016 Praise Worthy Prize - All rights reserved.

Keywords


Model Checking; Abstractions; Concurrent Systems

Full Text:

PDF


References


M. B. Dwyer, L. A. Clarke, J. M. Cobleigh, G. Naumovich, Flow Analysis for Verifying Properties of Concurrent Software Systems, ACM Transactions on Software Engineering and Methodology (TOSEM), Vol. 13, pp. 359-430, 2004.

S. F. Siegel, A. Mironova, G. S. Avrunin, L. A. Clarke, Using Model Checking with Symbolic Execution to Verify Parallel Numerical Programs, International Symposium on Software Testing and Analysis (ISSTA 2006), pp. 157-168, 2006.

D. Peled, H. Qu, Enforcing Concurrent Temporal Behaviors, Int. J. Found. Comput. Sci. Vol. 17, pp. 743-762, 2006.

K. Ostrovsky, On modelling and analysing concurrent systems, Ph.D. dissertation, Comp. Sc. And Elect. Eng., Chalmers University of Technology, Sweden, 2005.

E. Clarke, O. Grumberg, D. Peled, Model Checking (The MIT Press 2000).

S. Chouali, J. Julliand, P.-A. Masson, F. Bellegarde, PLTL Partitionned Model-Checking for Reactive Systems under Fairness Assumptions, ACM Transactions on Embedded Computing Systems (TECS), 4(2):267--301, 2005.

I. Rabinovitz, O. Grumberg, Bounded Model Checking of Concurrent Programs, International Conference on Computer Aided Verification (CAV'05), 2005.

P. Cousot, Abstract Interpretation, ACM Computing Surveys, Vol. 28, 1996.

E. Clarke, O. Grumberg, S. Jha, Y. Lu, H. Veith, Counterexample-guided abstraction refinement for symbolic model checking, J. ACM, 50(5):752-794, 2003.

R. Tzoref, O. Grumberg, Automatic Refinement and Vacuity Detection for Symbolic Trajectory Evaluation, International Conference on Computer Aided Verification (CAV'06), 2006.

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

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

D. Dams, R. Gerth, O. Grumberg, Abstract Interpretation of Reactive Systems, ACM Transactions on Programming Languages and Systems (TOPLAS), Vol. 19, 1997.

E. Clarke, O. Grumberg, D. Long, Model Checking and Abstraction, ACM Transactions on Programming Languages and Systems (TOPLAS), Vol. 16, 1994.

E. Clarke, E. Emerson, A. Sistla, Automatic Verification of Finite-state Concurrent Systems Using Temporal Logic Specifications, ACM Transactions on Programming Languages and Systems, Vol. 8, 1986.

E. Emerson, C. Lei, Efficient Model Checking in Fragments of the prepositional -calculus, In Proceedings of the First Annual Symposium of Logic in Computer Science, 1986.

R. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers, Vol. 35, 1986.

O. Grumberg, D. Long, Model Checking and Modular Verification, In CONCUR'91, LNCS, Springer, 1991.

M. Bourahla, M. Benmohamed., Predicate Abstraction and Refinement for Model Checking VHDL State Machines, Electronic Notes in Theoretical Computer Science, Elsevier Science B.V., Vol. 66, 2002.

M. Bourahla, M. Benmohamed., Abstract Model Checking Infinite State Systems, in AICCSA 2003, IEEE Computer Society, 2003.

M. Bourahla, M. Benmohamed., Verification of real-time systems by abstraction of time constraints, in IPDPS 2003, IEEE Computer Society, 2003.

K. McMillan, Symbolic model checking, (Kluwer Academic Publishers, 1993).


Refbacks

  • There are currently no refbacks.


Please send any question about this web site to info@praiseworthyprize.com
Copyright © 2005-2024 Praise Worthy Prize