Routing protocol

We consider a routing protocol that can work in two different environments: a safe environment, where all the nodes are fully trusted, and an unsafe environment, where some nodes might be corrupted. In an unsafe environment, a message must be encrypted before it is sent. Every operation (routing, sending and encryption) requires time to complete.

The protocol must satisfy safety and liveness properties. When the environment is unsafe, all the messages must be encrypted before they are sent. When the environment is safe, the messages must be sent at most 20 time units after being received. In a changing environment, the protocol must switch between the two configurations in order to adapt itself. This reconfiguration is only possible in state received. We study two different implementations: in the first one, the reconfiguration can occur at most every 25 time units; in the second one, the reconfiguration can always be done but its application requires 5 time units. We want to determine in which implementations the system can satisfy its specifications.routing_protocol

We model this systems using timed games with adaptive features (FTGA presented above). This allows to represent in a single model the different configurations of the system and the environment, as well as the possibility to change the configurations at runtime. The model is presented in the figure below.

  • The system actions are the dashed line transitions: route!, reconfig!
  • The environment actions are the continuous line transitions: init?, receive?, encryption?, sent?.
  • encrypt is a system adaptive feature that specifies in which operation mode the system currently is. To update the feature a variable new_encrypt is used.
  • Two static features preconf and treconf specifies which of the two reconfiguration methods the system can use. preconf allows the periodic reconfiguration, while treconf allows the non-atomic reconfiguration.
  • Finally, the environment is described with an adaptive feature safe that specifies whether the current node in the network can be trusted or not.
  • The system may only reconfigure the feature encrypt during the transitions labelled “reconfig“. Therefore on the other transitions the feature is updated with the expression: new_encrypt=encrypt, which means that the feature keeps its current value.
  • The environment may only reconfigure the feature safe during the transitions labeled “sent” and “receive”.

We check this example with PyECDAR during a tutorial. The property “If the environment is unsafe, all the messages must be encrypted before they are sent.” can be expressed by the T-AdaCTL formula

A[]([not safe] not RoutedSafe)

This formula specifies that the system can never reach the location RoutedSafe if the environment is not safe. We can check this property using PyECDAR. It computes the satisfaction relation for the formula, which is given by:

preconf or treconf or encrypt

It means that the formula is satisfied if and only if any of the two reconfiguration features are enabled, or feature encrypt is initially enabled.

The second property “If the environment is safe, the messages must be sent at most 20 time units after being received.” can be expressed by another the T-AdaCTL formula

A[]([safe] Received => A<>[0,20](Ready))

It specifies that whenever location Received is reached in a safe environment, the location Ready must be reached within 20 time units. We check this property with PyECDAR and we obtain the following result:

preconf or encrypt

Finally, we consider the formula

A[]([not safe] not RoutedSafe and [safe](Received => A<>F[0,20] RoutedSafe))

that combines the two previous ones. The satisfaction relation computed by PyECDAR is now restrained to preconf, which proves that in order to satisfy both properties at the same time the system requires the preconf feature.