$($e$)$ We modelled the amended protocol by a process System, specified its correctness by a

process SPEC, and checked its correctness by a suitable assertion:

SYSTEM send, receive $|$ USERS

SPEC$=$ kn$?n$: noncesI $$SPEC

assert SPEC System send, receive $|$

In the following, 'explain' means giving an informal explanation showing an under$-$

standing of the modelling.

$($i$)$ Explain what the process System means $($describe its components and explain the

way they are connected$).$

$($ii$)$ Explain what the assertion means. Explain all parts of it$,$ in particular, explain

the meaning of send, receive $|$ and why this part is necessary.

$($iii$)$ Which correctness property is guaranteed if the execution of this assertion suc$-$

cessfully terminates $($that is$,$ with the result "Passed"$)?$