XCD translator extension

Background

XCD is a language for describing architectures of component-based software systems. It allows to define different types of conditions for accepting method calls from other components and one can use the XCD translator to produce a model of their architecture in the ProMeLa language of the Spin model checker, so that they can verify it automatically.

The verification tool chain works like this:

  1. First, one produces a ProMeLa model for Spin from the XCD input architectural specification, using the XCD translator: 
    java -jar xcd.jar fileName.xcd
    This command produces a folder "src-gen" which includes a set of ProMeLa files representing the entire ProMeLa model of that XCD specification.
  2. Then you run SPIN to produce a verifier for the ProMeLa model: 
    cd src-gen
spin -a configuration.pml
  3. Then you compile the verifier: 
    gcc -O2 -DMEMLIM=7024 -o pan pan.c
  4. And finally you execute the verifier: 
    ./pan
Or in one shot: 
java -jar xcd.jar fileName.xcd \
&& (cd src-gen ; spin -a configuration.pml \
   && gcc -O2 -DMEMLIM=7024 -o pan pan.c \
   && ./pan)
Note the use of "&&" where the previous command may fail.

Tasks

  1. Simple - tidy up:
    1. Add code to a private github repository (link to be provided).
    2. Add some testing to check if the output produced for specific input files is the same as the respective output files we've got now.

      You can access the XCD case studies here (https://www.staff.city.ac.uk/c.kloukinas/Xcd/case_studies.html).

      A simple "diff -bw output_file_before output_file_now" would be sufficient (-bw means ignore whitespaces - useful for the change below).

    3. Clean up the code - delete all spaces after a backslash to get rid of warnings by cpp (cpp - The C PreProcessor - is used by Spin): 
      "...\\ ..." -> "...\\..."
    4. Clean up the code - create global definitions of labels and use these global variables where the actual strings are used now in the code: 
      String label_component = "COMPONENT_";
String label_connector = "CONNECTOR_";
String label_part = "PART_";
String label_role = "ROLE_";
String label_var = "VAR_";
...

      Check that when you do a "grep COMPONENT" on the source files the only results are these global labels (same for the other values too).

      Check that the output produced is still the same.

    5. Reduce label names to make very long names easier to read during verification: 
      String label_component = "CT_";
String label_connector = "CR_";
String label_part = "PT_";
String label_role = "RL_";
String label_var = "VR_";
...
    6. Make small changes to get rid of other warnings by Spin (move a few label goto targets in the output around basically).
  2. Extend:
    1. In Mert Ozkaya's PhD thesis, there's a pattern of ProMeLa/Spin code used for Required/Consumer/Provided ports (shown in Figure 3.12(b-d), p. 92, and Figures 3.15 and 3.16).

      This pattern is further described in section 4.4.6 (p. 123), detailing how "user-defined buffers" are used by a component to receive messages from other components - see also Listing 4.9 on p. 126 (and Listings 4.10-12).

      Essentially it's this: When component A sends a request/message to component B, B takes it out of the message channel queue and pushes it into a local buffer.

      Then B pops some message from its local buffer to see if it satisfies the predicates that would make it safe to treat this message/responding to this request. When it finds one, it removes it from the local buffer and treats it. This is described in detail in section 4.4.7.2 (p. 125).

      We had to use this convoluted pattern because Spin does not allow us to read a message from a message channel queue only when that message satisfies some condition/predicate, so we had to do it manually: 

              :: channel ? message // try to receive next message, if any.
           -> push_to_buffer(message) ; // called "push" in the pattern
        :: pop_from_buffer(message, conditions_A)
           -> if
              :: satisfies(message, conditions_B)
                 -> treat(message);
              :: else -> assert(false); // raise an error
              fi
        :: pop_from_buffer(message, conditions_C)
           -> assert(false); // raise an error

      Since then, another student has extended Spin so that we can now do such a "selective" message reception directly, without the use of an intermediate buffer: 

              :: channel ?? message : conditions_A &&    conditions_B
           -> treat(message);
        :: channel ?? message : conditions_A && (! conditions_B)
           -> assert(false); // raise an error
        :: channel ?? message : conditions_C /* NOTE: ?? receives the
             first message that matches the conditions - not necessarily
             the first message in the channel queue. */ 
           -> assert(false); // raise an error

      What we want now is to change the code in the Xcd translator so that it uses this second pattern, so as to take advantage of the extended Spin's functionality.

  3. Experiment:
    1. Run the extended translator on all the existing input files, get the new output files and use the extended Spin to verify them. (you'll just be executing two programs for each input file).
    2. Compare the reported (a) size of the state vector (description of the current state of the model); (b) number of states produced; (c) number of transitions produced; and (d) overall RAM usage during verification, against the values we have now.

      We expect a significant reduction in the number of states/transitions/memory but we cannot know how much we'll gain without doing these experiments.

Info