Hello ! I read an article named Model-Based Security Analysis of a Water Treatment System . It models an example of water level control using an earlier version of alloy, but I don’t know how to modify it to make it work properly in alloy6. I would appreciate if some kind person would suggest something.
open util/ordering[Tick] // Create a total ordering of global ticks
sig Tick {}
/**Generic part of a system model **/
abstract sig PhysicalProcess {state: PhysicalState one -> Tick}
abstract sig Sensor {process: PhysicalProcess}
abstract sig Actuator {state: ActuatorState one -> Tick}
abstract sig PLC{
sensors: set Sensor, actuators: set Actuator, processes: set PhysicalProcess,
//At every tick，PLC reads states information from its sensors and actuators
reads : (Sensor + Actuator) -> (State one -> Tick)
}
sig Compromised in Sensor + Actuator {}//Some of the sensors and actuators are compromised
/**SWaT-specific part of the model **/
one sig On,Off extends ActuatorState {}
abstract sig LevelState extends PhysicalState {}//State of water level in a tank
one sig UF,LL,L2,L1,L,H,H1,H2,HH,OF extends LevelState {}//UF underflow,OF overflow
//SWaT components for Stage P1
one sig RawWaterTank extends PhysicalProcess {}
one sig LIT101 extends Sensor {} {process = RawWaterTank}
one sig P101,MV101 extends Actuator {}
one sig PLC1 extends PLC {}{
sensors = LIT101 + FIT101 and
actuators = P101 + MV101 and
processes = RawWaterTank
}
//Describes how the state of the water tank changes given the status of actuators
pred transition_RawWaterTank[t, t' :Tick]{
let pre = state.t,post = state.t' {
MV101.pre= On and P101.pre =On implies this.post =this.pre
MV101.pre= On and P101.pre =Off implies this.post =increaseLevel[this.pre]
MV101.pre= Off and P101.pre =On implies this.post =decreaseLevel[this.pre]
MV101.pre= Off and P101.pre =Off implies this.post =this.pre }}
//Describes how the state of MV101 changes given PLC1 sensor readings
pred transition_MV101[t , t': Tick]{
let plc1readings =PLC1.reads.t,pre =state.t,post= state.t'{
plc1reading [LIT101]=H implies MV101.post =Off
plc1readings [LIT101]=L implies MV101.post =On
else MV101.post= MV101.pre }}
fact CompromisedBehavior{
//Sensor reading matches the actual state of the physical process if sensor is not compromised
all s: Sensor,p :PLC,t :Tick | s not in Compromised implies (p.reads.t)[s] = s.proces.(state.t)
//Reading from the actuator matches its actual state if it is not compromised
all a: Actuator,p: PLC,t: Tick | a not in Compromised implies (p.reads.t)[a] = a.state.t
//MV101 follows expected state changes if it is not compromised
all t :Tick - last | let t' =t.next| MV101 not in Compromised implies transition_MV101[t,t']
}
/**Safety property**/
//True iff system detects overflow or unexpected level changes in the raw water tank
pred alarm_tankMonitor [t : Tick]{
let t0= t.prev,readings =(PLC1.reads.t0),level=readings[LIT101],
level'=(PLC1.reads.t)[LIT101]
|(level'=HH) or //reading indicates that water is about to overflow
(readings[MV101]=On and readings[P101]=On and level'!=level) or
(readings[MV101]=On and readings[P101]=Off and level'!=increaseLevel[level]) or
(readings[MV101]=Off and readings[P101]=On and level'!=decreaseLevel[level]) or
(readings[MV101]=Off and readings[P101]=Off and level'!=level)}
//True iff water overflows and no alarm is triggered
pred unsafe[t: Tick] {RawWaterTank.state.t = OF and no alarm_tankMonitor[t.prevs]}
//pred unsafe[t: Tick] {RawWaterTank.state.t = OF }
//System should never reach an unsafe state
assert SystemIsSafe{ no t :Tick | unsafe [t]}