Home > Articles > Programming > General Programming/Other Languages

An Overview of PROMELA

This chapter is from the book 

Reading Input

On an initial introduction to PROMELA it may strike one as odd that there is a generic output statement to communicate information to the user in the form of the printf, but there is no matching scanf statement to read information from the input. The reason is that we want verification models to be closed to their environment. A model must always contain all the information that could possibly be required to verify its properties. It would be rather clumsy, for instance, if the model checker would have to be stopped dead in its tracks each time it needed to read information from the user’s keyboard.

Outputs, like printf, are harmless in this context, since they generate no new information that can affect future behavior of the executing process, but the executing of an input statement like scanf can cause the modification of variable values that can impact future behavior. If input is required, its source must always be represented in the model. The input can then be captured with the available primitives in PROMELA, such as sends and receives.

In one minor instance we deviate from this rather strict standard. When SPIN is used in simulation mode, there is a way to read characters interactively from a user-defined input. To enable this feature, it suffices to declare a channel of the reserved type STDIN in a PROMELA model. There is only one message field available on this predefined channel, and it is of type int. The model in Figure 3.2 shows a simple word count program as an example.

Figure 3.2 Word Count Program Using STDIN Feature

chan STDIN;
int c, nl, nw, nc;

init {
       bool inword = false;

       do
       :: STDIN?c ->
                  if
                  :: c == -1 ->
                          break /* EOF */
                  :: c == '\n' ->
                          nc++;
                          nl++
                  :: else ->
                          nc++
                  fi;
                  if
                  :: c == ' '
                  || c == '\t'
                  || c == '\n' ->
                          inword = false
                  :: else ->
                          if
                          :: !inword ->
                                  nw++;
                                  inword = true
                          :: else /* do nothing */
                          fi
                  fi
          od;
          assert(nc >= nl);
          printf("%d\t%d\t%d\n", nl, nw, nc)
}

We can simulate the execution of this model (but not verify it) by invoking SPIN as follows, feeding the source text for the model itself as input.

$ spin wc.pml < wc.pml
27      85         699
1 process created

PROMELA supports a small number of other special purpose keywords that can be used to fine-tune verification models for optimal performance of the verifiers that can be generated by SPIN. We mention the most important of these here. (This section can safely be skipped on a first reading.)

InformIT Promotional Mailings & Special Offers

I would like to receive exclusive offers and hear about products from InformIT and its family of brands. I can unsubscribe at any time.