PLTL Partitioned Model Checking for Reactive Systems under Fairness Assumptions

Details PLTL Partitioned Model Checking for Reactive Systems under Fairness Assumptions PLTL Partitioned Model Checking for Reactive Systems under Fairness Assumptions

2006-02-10

arxiv.org/abs/cs/0602040v1

ACM Transactions on Embedded Computing Systems 4(2) (2005) 267-301

Computer Science

Logic in Computer Science

Scientific paper

10.1145/1067915.1067918

We are interested in verifying dynamic properties of finite state reactive systems under fairness assumptions by model checking. The systems we want to verify are specified through a top-down refinement process. In order to deal with the state explosion problem, we have proposed in previous works to partition the reachability graph, and to perform the verification on each part separately. Moreover, we have defined a class, called Bmod, of dynamic properties that are verifiable by parts, whatever the partition. We decide if a property P belongs to Bmod by looking at the form of the Buchi automaton that accepts the negation of P. However, when a property P belongs to Bmod, the property f => P, where f is a fairness assumption, does not necessarily belong to Bmod. In this paper, we propose to use the refinement process in order to build the parts on which the verification has to be performed. We then show that with such a partition, if a property P is verifiable by parts and if f is the expression of the fairness assumptions on a system, then the property f => P is still verifiable by parts. This approach is illustrated by its application to the chip card protocol T=1 using the B engineering design language.

Affiliated with

Also associated with

No associations

Rating

PLTL Partitioned Model Checking for Reactive Systems under Fairness Assumptions does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with PLTL Partitioned Model Checking for Reactive Systems under Fairness Assumptions, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and PLTL Partitioned Model Checking for Reactive Systems under Fairness Assumptions will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-599986