Formal Evaluation of the HSF-CN
Formal verification is the process of employing formal methods to check whether a system meets its intended specifications (behavior). In the case of the developed HSF-CN, the behavior concerns the correct behavior of the developed algorithms for initialization, routing, and reporting. In contrast to testing and simulative methodologies, formal method techniques perform an exhaustive search of the state space of the model, thereby providing full guarantees of correctness.
Model checking is a popular approach towards formal verification [84]. It is fully automated and it is supported by model checking toolkits that have been developed and applied to various industrial settings, such as hardware verification and safety-critical systems. In model checking, a system is represented as a semantical structure or a model, and a property is encoded as a logic formula. The modelchecking problem is to check whether the model satisfies the formula, thereby establishing the satisfaction of the property by the system. The key limitation of model checking is the state-space explosion problem: the state space of the system grows exponentially in the number of variables encoding the system.
In the context of our analysis, we employed the model checker tool UPPAAL [29] to exhaustively check the state space of particular HSF-CN designs. Such exhaustive checks of the executions led to the identification of subtle cases where bugs and/or deadlocks were present. The model checker also supports Statistical Model Checking techniques to approximate the distributions of metrics, e.g., the distribution of the time needed to cover the entire HSF, and alleviate the state-space explosion problem in the analysis of demanding scenarios (e.g., larger topologies).
The evaluation of the HSF-CN begins with the development of an UPPAAL model of the HSF. The model is a set of timed automata that describe the behavior of the controller and the GW. For per-
Figure 5.6 The Parameters used for representing some characteristics of the network for a simulation.
forming model checking experiments, the Statistical Model Checking (SMC) module of the UPPAAL tool was used. Statistical model checking allows for checking a statistical sample of the model’s state space to deal with the state-space explosion problem. The main model checking experiment done was for checking that the design (parameters and routing algorithm) was deadlock-free in the presence of multiple packets being routed simultaneously. The query simply asked for the total number of acknowledgment packets after the end of the execution. The case where not all acknowledgment packets are received is an indicator for the presence of a deadlock. A second experiment queries the total clock time of an execution and it is used to measure performance. These properties are checked using the following form of SMC queries:
where timesteps is the number of time-steps each execution trace is run; times is the number of traces being analyzed and property is the property under investigation. Model checking results were an important tool in the process of developing the final HSF design. Through an iterative process, several designs of the HSF were proposed and were formally evaluated using the SMC. For example, in the case where a problem, e.g., a deadlock, was found using the SMC, a non-statistic model checking experiment was run that could generate the problematic trace and instance. Based on the trace analysis the design team could then suggest an alternative design by changing the parameters of the model. Formal evaluation as part of the design process complements the use of simulation testing software, since it can be easily deployed to exhaustively check all the possible execution interleaving. Model checking has led to the collection of valuable information about necessary and/or sufficient conditions for deadlocks in other topology configurations. This information can lead to a more efficient usage of more advanced configurations in the future [84].
The UPPAAL timed state machine of the switch controller is presented in Fig. 5.7. In addition, the functionality of the Gateway is described by a separate state machine. A set of state machines that interact using input/output actions constitute the model of the HSF. The controller state machine has two states (idle and processing) and can perform input/output actions on two input channels and two output channels. At the idle state, the controller waits for an interaction on one of the two input actions that indicated the receipt of a packet. Upon such an interaction, the machine proceeds to the processing state and at the same time receives and buffers the packet. At the processing state, there are several actions that might be enabled. Firstl}r, the
Figure 5.7 UPPAAL State Machine for the Switch Controller.
input actions are enabled in the case where there exists buffer space and more packets can be received. At the processing state, the first packet from the buffer is being inspected and if its routing target is a different controller then the corresponding output action is enabled following the routing algorithm. If the packet’s routing target is the current controller, then the packet is consumed and an acknowledgment packet is prepared and routed accordingly. Each transition, if enabled, requires a clock tick to be completed. Clock ticks allow for counting time, thus having a metric for measuring performance. The model was designed so it can be adjusted for several parameters. The main parameters that interest the current evaluation are: the network size, the routing sequence of packets, the position of the Gateways, and the buffer size. The formal evaluation methodology together with the obtained results for particular scenarios appear in [84].
