1. Home
  2. Model checking concurrent
  3. Model checking concurrent
  4. Using temporal logic to specify

0.5 Using temporal logic to specify properties  (Page 8/11)

<< Chapter < Page
  Model checking concurrent     Page 8 / 11
Chapter >> Page >

We've previously seen that SPIN knows some built-in concepts such as deadlock , livelock , weak- andstrong- fairness . We'll see in the next section that SPIN can also be used to verify any LTL formula. But first, let's characterize some of those built-inconcepts as LTL formulas using the context of a print server.

We will use the following propositions:

  • b : This is a bad state. (It corresponds to Promela assert(! b ) ).
  • e : This is a valid end state. (It corresponds to all Promela processes being atan end label).
  • p 1 , p 2 : Progress is being made (either of two types of progress);they correspond to a Promela process being at a certain progress label.
    Promela does includes a handy syntax for testing whether a particular processis at a particular label: `` philosopher[3]@eating '' is true when the fourth (0-indexed) philosopher process is at the label eating .
  • r : There is a pending request.
  • s : A request is being serviced.
Give a temporal formula expressing each of the following:

  • No error occurs, i.e. , we never reach a bad state.
  • No deadlock occurs.(We'll take deadlock here to mean that all five of our variables stop changing;without having a different proposition for each state, this is close enough.)
  • Progress is always made.That is, this trace doesn't go forever without making progress.
  • Weak Fairness:if a request is made and held, it will get serviced. I.e. , it's not the case that a request stays forever but is never serviced.
  • Strong Fairness:if a request is made infinitely often, then it will be serviced.

For each of these problems, there are many equivalent formulas,some of which are easier to verify as equivalent than others.

  • □ b
  • ◇ ( ( □ b □ b ) ( □ p □ p ) ( □ r □ r ) ( □ s □ s ) □ e ) . Remember that if we're in an end-state, then it doesn'tcount as deadlock.
  • □ ◇ ( p 1 p 2 ) ( □ ◇ p 1 □ ◇ p 2 ) . In fact, SPIN provides a built-in variable np_ , which corresponds to``all processes are in a non-progress state''. When SPIN does its built-in check for non-progress cycles,it actually just verifying !<>[]np_ . You might recall that SPIN's idea of progress is state-based, not transition-based:SPIN (counterintuitively) considersit progress when a process does nothing but squat in a progress state. (This can only happen if weak fairness is not beingenforced, or a guard is being labeled as progress.) How might we capture ``progress'' but stillpreclude those traces which just sit idly at a progress label? We could add a second progress label immediately following p 1 , call it q 1 . Similarly, we can introduce q 2 . Then we could verify that ( ( □ ◇ p 1 □ ◇ q 1 ) ( □ ◇ p 1 □ ◇ q 1 ) ) . (This assumes that all labels are private to each process.)
  • ``It's always not the case that r is always on, and yet s doesn't happen an infinite number of times'': □ ( □ r □ ◇ s ) . One equivalent formula is``if r stays on forever, then it's being serviced infinitely often.'': □ ( □ r □ ◇ s ) .
  • ( □ ◇ r □ ◇ s )
<< Chapter < Page Page > Chapter >>

Read also:

Get Jobilize Job Search Mobile App in your pocket Now!

Get it on Google Play Download on the App Store Now




Source:  OpenStax, Model checking concurrent programs. OpenStax CNX. Oct 27, 2005 Download for free at http://cnx.org/content/col10294/1.3
Google Play and the Google Play logo are trademarks of Google Inc.

Notification Switch

Would you like to follow the 'Model checking concurrent programs' conversation and receive update notifications?

Ask