loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05)
Stuttering Abstraction for Model Checkin
Koblenz, Germany
September 07-September 09
ISBN: 0-7695-2435-4
Shiva Nejati, University of Toronto, Canada
Arie Gurfinkel, University of Toronto, Canada
Marsha Chechik, University of Toronto, Canada
Abstraction is one of the most effective approaches to improving the applicability and the scalability of modelchecking. The goal of abstraction is to construct a model which is small enough to analyze, yet contains enough detail to allow conclusive analysis of properties of interest. For a given concrete model, the size of its smallest possible abstraction is intimately related to the set of temporal properties preserved by the abstraction. Thus, smaller abstractions are possible if we reduce this set, for example, by disallowing the use of the next-time operator. In this paper, we improve the conclusiveness and efficiency of the 3-valued abstraction framework. We start by proposing a number of simulation relations that preserve true properties expressed in subsets of CTL without the next-time operator. We show how these simulation relations are extended into refinement relations for defining 3-valued abstractions. Using these refinement relations, we give a new abstraction method that results in more conclusive abstract models.
Citation:
Shiva Nejati, Arie Gurfinkel, Marsha Chechik, "Stuttering Abstraction for Model Checkin," sefm, pp.311-320, Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05), 2005
Usage of this product signifies your acceptance of the Terms of Use.