The experiments

The experiments

We provide in the subdirectory steamboiler a Makefile and two scripts to execute the experiments with nbacg.opt executable.

We ran nbacg.opt with the option file .nbacrc:

nbacg.opt -rc .nbacrc -print "+p +r" System.ba

The global model has 63 Boolean or enumerated state variables, and 7 real variables. (However, if one forbids failure to occur, most of these Boolean variables will become constants, as they are related to the error protocol.) It has also a dozen of Boolean input variables encoding the non-determinism of various failure occurences.

The initial control structure is the control structure of process X (scheduler). We then ask (with the control statement) to distinguish the physical states of the pumps. This is the "guided refinement" step. Then further refinement is performed by our standard heuristics.

We tried to check the basic safety property (namely, the physical water level is between the constants 150 and 850, the total capacity of the tank being C=1000) under various assumptions about the occurence of failures. For each assumption, we check separately the lower bound (min) and upper bound (max) properties.

1. No failure at all.
2. Possible failure of pump 0, for any time duration.
3. Possible failure of steam flow device, for any time duration.
4. Possible failure of water level device, during atmost 20s separated by at least 40s

The experiments