Supplementary Material (FM 2016 Paper)
This page contains supplementary material for our short paper, Towards Learning and Verifying Invariants of Cyber-Physical Systems by Code Mutation (DOI), published at FM 2016.
Mutations
The negative traces used for learning were generated by the SWaT simulator running under six different mutations. The code of the SWaT simulator is not yet available online, but we summarise the six mutations and their locations below. The identifiers in brackets correspond to the filenames of the negative traces also available on this webpage.
- Mutant One (plc1f): in PLC 1, the assignment HMI.P101.Permissive[1] = HMI.MV201.Status == 2 was mutated to HMI.P101.Permissive[1] = HMI.MV201.Status == 1.
- Mutant Two (plc2c): in PLC 2, the guard of an if-statement HMI.P2.State==1 was mutated to HMI.P2.State==2.
- Mutant Three (plc3b): in PLC 3, an assignment HMI.MV303.Auto = 0 was mutated to HMI.MV303.Auto = 1.
- Mutant Four (plc3d): in PLC 3, the guard of an if-statement HMI.P4.State == 1 was mutated to HMI.P4.State == 2.
- Mutant Five (plc3e): in PLC 3, the guard of an if-statement case(1) was mutated to case(2).
- Mutant Six (plc4a): in PLC 4, an assignment HMI.P3.State=2 was mutated to HMI.P3.State=1.
SWaT Training Data
The positive and negative traces of sensor data obtained from the SWaT simulator are available to download below.
The traces log the water levels of the five (simulated) tanks in SWaT over 30 minutes.
The positive traces were obtained from the SWaT simulator without mutations. The files normalX.txt contain traces resulting from three different initial states X (i.e. different initialisations of water tank levels).
The negative traces were obtained from the SWaT simulator under the six mutations (each in isolation). The files <ID>X.txt contain traces resulting from initial state X under the mutant with identifier ID.
Classifier
The classifier presented in the paper only gives the coefficients to three decimal places. The full classifier we learnt is as follows:
-0.3492853062583663 v_1
9.78873712411496 v_2
-10.191567805729619 v_3
0.8031654936094128 v_4
-5.560554789806133 v_5-0.6298698273967602 v_1′
-10.455262029320693 v_2′
10.333015684807378 v_3′
0.8031654936094128 v_4′
3.9283341201904705 v_5′rho = -786.4158631412631
The variables v_1, … v_5 and v_1′, … v_5′ denote the water levels of the five tanks at 250ms apart.