Examples of I&C design issues found with model checking
I've collected design issues detected in real-world industry projects on this page. In case you'd like to try and figure out what the problem is, I've hidden the counterexamples behind the "Show / Hide counterexample" link.
For each issue, you can find a link to my publication with the details. Please cite the source if you use these examples in your own work.
The examples are masked and simplified to mask their origin. I've only included the blocks needed to reproduce the issue, but the original model was typically way more complex.
All the issues were detected with NuSMV.
Example 1
Keywords: memory, operator action
The logic is for locking a point to the end it is in, if there are conflicting requests to move towards both ends.
The black triangle in the RS block means that it is of the "retain" type, and will store its state even if the PLC logic goes offline.
| Requirement: | After the conflict in orders is resolved, the point shall be free to move towards the requsted end (Lock is reset). |
| Failing property: | G (((At_A ∧ Request_to_A ∧ Request_to_B) ∧ X (At_A ∧ ¬Request_to_A ∧ Request_to_B) → X ¬ Lock) |
| Blocks in original model: | 784 |
The issue was found using bounded model checking (BMC).
Citation: Pakonen, A., Turunen, J. Using model checking for interlocking software verification, SIGNAL+DRAHT, Volume 115, Issue 9, September 2023.
The counterexample has four steps:
- The point has been requested to move to end B, it has reached end B, and is locked there.
- The PLC running the logic goes offline. While the PLC is offline, the point is manually forced to end A (which is a maintenance action that sometimes takes place).
- Then the PLC returns online, it does so under circumstances where conflicting requests are active. The "at B" RS block retains its state.
- The conflict in requests is then resolved, but the point is still locked, due to the retained "at B" state.
This is an illustrative counterexample, having features that are not easily thought of when specifying test cases. It has several unlikely and unrelated events, occuring in a specific order, happening around the same time.
Example 2
Keywords: memory, feedback loop, operator action
| Requirement: | Both MODE_A and MODE_B shall not be set at the same time. |
| Failing property: |
G ¬(MODE_A ∧ MODE_B
) |
| Blocks in original model: | 57 |
| Reachable states in original model: | 5,5 • 108 |
Citation: Pakonen, A., Tahvonen, T., Hartikainen, M., Pihlanko, M. Practical applications of model checking in the Finnish nuclear industry, 10th ANS International Topical Meeting on Nuclear Plant Instrumentation, Control, and Human-Machine Interface Technologies (NPIC & HMIT 2017), June 11-15, 2017, San Francisco, CA, USA, pp. 1342-1352.
Due to the feedback loop, the logic requires a cycle delay element (TC). The idea of the logic is that MODE_A is reset if (1) SET_B is set, or (2) AUTO_B is set. Here, on step 2, AUTO_B does not reset MODE_A due to the cycle delay. On the next cycle (step 3), AUTO_B is reset, so MODE_A remains set.
Example 3
Keywords: memory
| Requirement: | If VAR drops to a value below 10, ACT shall be set. |
| Failing property: |
G ((VAR > 10
) ∧ X (VAR < 10
) → X ACT) |
| Blocks in original model: | 60 |
| Reachable states in original model: | 5,4 • 1018 |
Citation: Pakonen, A. Oops! Examples of I&C design issues detected with model checking, International Symposium on Future I&C for Nuclear Power Plants (ISOFIC 2021), November 15-17, 2021, Okoyama, Japan (hybrid online/offline event).
In the counterexample, VAR drops from a value above 10 immediately (within a processing cycle) to a value below 8 (which in the original context is highly unlikely).
Example 4
Keywords: memory, operator action, validity
This logic involves signal status processing — each signal wire carries an additional "fault bit" indicating if an error has occured in the upstream logic. The "2nd Max" block will only considered valid (not faulty) signals, and set the F output, if too many inputs have failed.
| Requirement: | Control shall not be based on a faulty setpoint. |
| Failing property: | G ¬((2MAX = 0) ∧ ¬2MAX_FAULT) → G ¬((SETPOINT = 0) ∧ ENABLE)) |
| Blocks in original model: | 73 |
| Reachable states in original model: | 4,6 • 1018 |
Citation: Pakonen, A., Buzhinsky I., Björkman K. Model checking reveals design issues leading to spurious actuation of nuclear instrumentation and control systems, Reliability Engineering & System Safety, Volume 205, January 2021, 107237. 10.1016/J.RESS.2020.107237
In the counterexample, the logic is initialised to a state where too many redudant Measurement signals have failed, so the "2nd Max" block outputs the default preset intial value of zero. Next, the logic receives enough valid Measurement signals to switch the fault state off, but the simultaneous CTRL_ON signal causes the default preset value of zero to be stored as the setpoint, leading the logic to spuriously set the CLOSE command.
Example 5
Keywords: delay, memory, feedback loop, operator action, frozen
| Requirement: | If ACT_A is set, and then, within 5 seconds, SET_B is active, ACT_A is reset. |
| Failing property: | G (ACT_A → X X X X ((¬ SET_A ∧ SET_B ) → ¬ ACT_A )) |
| Blocks in original model: | 17 |
| Reachable states in original model: | 1,4 • 106 |
Citation: Pakonen, A. Oops! Examples of I&C design issues detected with model checking, International Symposium on Future I&C for Nuclear Power Plants (ISOFIC 2021), November 15-17, 2021, Okoyama, Japan (hybrid online/offline event).
In the (counterintuitive, in the original context) scenario where SET_B is not active within the five-second time window after ACT_A's actuation, the logic ends up in a state where ACT_A is permanently set and ACT_B is permanently reset.
The issue is also revealed by specifying the CTL reachability property AG EF ¬ ACT_A, or AG EF ACT_B.
Example 6
Keywords: memory, operator action
The logic is for ensuring that only one of three redundant subsystems can be inhibited (disconnected from controlling the process for testing or maintenance purposes) at a time.
| Requirement: | The redundant subsystems shall not be inhibited at the same time. |
| Failing property: | G ¬(INH_1 ∧ INH_2 ∧ INH_3 ∧ One_INH ) |
| Blocks in original model: | 49 |
| Reachable states in original model: | 9,9 • 1014 |
Citation: Pakonen, A. Model-checking I&C logics — practical examples, 13th Nuclear Plant Instrumentation, Control, and Human-Machine Interface Technologies (NPIC & HMIT 2023), July 15-20, 2023, Knoxville, TN, USA, pp. 1610-1619. 10.13182/NPICHMIT23-41122
In the counterexample, the first subsystem is first inhibited (INH_1) by the operator using a switch (SWT_1). Then, SWT_2 is set at exactly the same time SWT_1 is reset. Then, SWT_3 is set at exactly the same time SWT_3 is reset.
As a result, the logic will only ever "see" one active switch, allowing for the inhibition of all three subsystems at the same time.
Example 7
Keywords: memory, operator action
| Requirement: | On the falling edge of ON, ACTIVE shall be reset. |
| Failing property: |
G (ON ∧ X ¬ON
→ X ¬ACTIVE) |
| Blocks in original model: | 29 |
| Reachable states in original model: | 4,3 • 1011 |
Citation: Pakonen, A., Björkman, K. Model checking as a protective method against spurious actuation of industrial control systems, 27th European Safety and Reliability Conference (ESREL 2017), June 18-22, 2017, Portoroz, Slovenia.
If the contrary inputs ON and STOP are both set, and then both are reset on the same processing cycle, there will not be a rising edge on the signal from the OR gate, so the SR memory (and, therefore, ACTIVE) remains set.
Example 8
Keywords: memory, operator action
| Requirement: | CRITERIA shall lead to ALARM. |
| Failing property: | G ((¬ALARM ∧ ¬CRITERIA) ∧ X (CRITERIA ∧ ¬ACK) → X ALARM) |
| Blocks in original model: | 65 |
| Reachable states in original model: | 4,9 • 1021 |
Citation: Pakonen, A., Buzhinsky, I., Vyatkin, V. Counterexample visualization and explanation for function block diagrams, 16th International Conference on Industrial Informatics (INDIN 2018), July 18-20, 2018, Porto, Portugal, pp. 747-753. 10.1109/INDIN.2018.8472025
If ACK is set even before the ALARM has occurred, and the CRITERIA is then set, ALARM is not set, even after ACK resets. (The alarm has been effectively acknowledged "in advance".)
Example 9
Keywords: memory
| Requirement: | CRITERION shall lead to TRIP until MANUAL ACK is set. |
| Failing property: | G (CRITERION ∧ H ¬ MANUAL_ACK) → TRIP) |
| Blocks in original model: | 24 |
| Reachable states in original model: | 1,1 • 108 |
Citation: Pakonen, A., Biswas, P., Papakonstantinou, N. Transformation of non-standard nuclear I&C logic drawings to formal verification models, 46th Annual Conference of the IEEE Industrial Electronics Society (IECON 2020), October 18-21, 2020, Singapore (held virtually), pp. 697-704. 10.1109/IECON43393.2020.9255176
Here, CRITERION is set on the intial state. Since the RS memory is set on the intial state by default, the result is that TRIP is prevented even if MANUAL ACK is not set.
Example 10
Keywords: memory, operator action
| Requirement: | |
| Failing property: | G (((ACTUATE ∧ HIGH_SETPOINT ∧ ¬RESET) X ∧ (NORMAL_TEMP ∧ RESET)) → X LOW_SETPOINT) |
| Blocks in original model: | 56 |
| Reachable states in original model: | 6,6 • 1013 |
Citation: Pakonen, A. Model-checking of I&C logics — insights from over a decade of projects in Finland, 12th ANS International Topical Meeting on Nuclear Plant Instrumentation, Control, and Human-Machine Interface Technologies (NPIC & HMIT 2021), June 14-17, 2021, Providence, RI, USA (held virtually), pp. 792-801. 10.13182/T124-34322
Example 11
Keywords: delay, feedback loop
| Requirement: | |
| Failing property: | |
| Blocks in original model: | 58 |
| Reachable states in original model: | 6,1 • 1032 |
The cycle delay block has a user-configurable initial output value, which had been set to zero. On initialisation, the switch component therefore outputs the value zero for a minimum of ten seconds until the correction can take effect. Assuming that the allowed level and the calculated level are both positive, non-zero numbers, both of the sum blocks will then output a negative value. A negative value cannot be over 5%, so the ACT output is effectively inhibited for the ten seconds after initialisation, no matter how high the measured level is above the allowed level.
Citation: Pakonen, A. Model-checking infinite-state nuclear safety I&C systems with nuXmv, 19th IEEE International Conference on Industrial Informatics (INDIN 2021). July 21-23, 2021, Palma de Mallorca, Spain (held virtually). 10.1109/INDIN45523.2021.9557445
Example 12
Keywords: delay
| Requirement: | |
| Failing property: | G (¬CRITERION ∧ X CRITERION →ACT) |
| Blocks in original model: | 2 |
| Reachable states in original model: | 104 |
Citation: Pakonen, A. Oops! Examples of I&C design issues detected with model checking, International Symposium on Future I&C for Nuclear Power Plants (ISOFIC 2021), November 15-17, 2021, Okoyama, Japan (hybrid online/offline event).
Example 13
Keywords: delay
| Requirement: | |
| Failing property: | G ((COND ∧ HIGH_P ) ∧ X (COND ∧ ¬ HIGH_P ) → X (CLOSE ∧ ¬ OPEN)) |
| Blocks in original model: | 6 |
| Reachable states in original model: | 3940 |
Citation: Pakonen, A. Oops! Examples of I&C design issues detected with model checking, International Symposium on Future I&C for Nuclear Power Plants (ISOFIC 2021), November 15-17, 2021, Okoyama, Japan (hybrid online/offline event).
Example 14
Keywords: delay
| Requirement: | |
| Failing property: | G (COND ∧ X ¬COND → X STOP ) |
| Blocks in original model: | 156 |
| Reachable states in original model: | 3,3 • 1038 |
Citation: Pakonen, A. Oops! Examples of I&C design issues detected with model checking, International Symposium on Future I&C for Nuclear Power Plants (ISOFIC 2021), November 15-17, 2021, Okoyama, Japan (hybrid online/offline event).
Example 15
Keywords: feedback loop, operator action
| Requirement: | |
| Failing property: | G ¬(INH_1 ∧ INH_2 ) |
| Blocks in original model: | 118 |
| Reachable states in original model: | 2,2 • 1024 |
Citation: Pakonen, A. Oops! Examples of I&C design issues detected with model checking, International Symposium on Future I&C for Nuclear Power Plants (ISOFIC 2021), November 15-17, 2021, Okoyama, Japan (hybrid online/offline event).
Example 16
Keywords:
| Requirement: | |
| Failing property: | G ¬(START ∧ STOP ) |
| Blocks in original model: | 19 |
| Reachable states in original model: | 2,7 • 1017 |
Citation: Pakonen, A. Oops! Examples of I&C design issues detected with model checking, International Symposium on Future I&C for Nuclear Power Plants (ISOFIC 2021), November 15-17, 2021, Okoyama, Japan (hybrid online/offline event).
Example 17
Keywords: memory, feedback loop, operator action
| Requirement: | |
| Failing property: | G ¬(CTRL_A ∧ CTRL_B ) |
| Blocks in original model: | 58 |
| Reachable states in original model: | 3,6 • 1019 |
Citation: Pakonen, A. Model-checking I&C logics — practical examples, 13th Nuclear Plant Instrumentation, Control, and Human-Machine Interface Technologies (NPIC & HMIT 2023), July 15-20, 2023, Knoxville, TN, USA, pp. 1610-1619. 10.13182/NPICHMIT23-41122
Example 18
Keywords: delay, frozen
| Requirement: | |
| Failing property: | |
| Blocks in original model: | 65 |
| Reachable states in original model: | 8,0 • 108 |
The IN2 signal has no effect on the downstream logic, because the on-delay element would require its input to be TRUE for over five seconds, but the pulse element only outputs the VALUE true for exactly five seconds.
Citation:
Pakonen, A.
Obfuscation of function block diagrams,
28th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA 2023), September 12-15, 2023, Sinaia, Romania.
10.1109/ETFA54631.2023.10275363
Example 19
Keywords: memory, delay, operator action
| Requirement: | |
| Failing property: | never {ACT [*n]} |
| Blocks in original model: | 13 |
| Reachable states in original model: | 3,6 • 105 |
Citation: Pakonen, A., Buzhinsky, I., Vyatkin, V. Evaluation of visual property specification languages based on practical model-checking experience, Journal of Systems and Software, Volume 216, October 2024, 112153. 10.1016/j.jss.2024.112153
Example 20
Keywords: memory, delay, operator action
| Requirement: | |
| Failing property: | always {(START & COND2);!COND2[*n ]} |-> {START}! |
| Blocks in original model: | 8 |
| Reachable states in original model: | 2,7 • 106 |
Citation: Pakonen, A., Buzhinsky, I., Vyatkin, V. Evaluation of visual property specification languages based on practical model-checking experience, Journal of Systems and Software, Volume 216, October 2024, 112153. 10.1016/j.jss.2024.112153
