# NOVA Mobility Assistive System: Developed and Remotely Controlled with IOPT-Tools
## 5 Prototypes
### Development Approach  
The proposed model-based development approach is supported by the IOPT-Tools framework. Models are created in the IOPT model edition tool, as presented in Figure 5, which contains the model of the controller of the NWCP module. The second step of the approach is the model simulation and its correction/optimization. The IOPT simulator is shown in Figure 6, presenting the model of the controller of the NWBP module. In the presented simulation, the module is initialized and it has two connections from other NWBs.  
Because, through simulations, it is not possible to ensure that the models are free from specification errors, in the third step of the proposed approach, the models' proprieties are verified using the IOPT model checking tools, which include a state-space generator tool and a query engine. The generated state-space graph, of the controller of the NWBP module, is partially presented in Figure 7. It is possible to verify, for example, the controller total number of states/nodes and the existence of deadlocks (this model has 253 possible states and is deadlock free). Given that, controllers usually have large state-spaces, often with millions of states, and it is not possible for humans to visually inspect it. The IOPT-Tools offer query tools to specify queries about the state-space to overcome this limitation. For example, in Figure 8, two queries are specified, in order to check whether the module accepts five or more connections from other NWBs. The query results (Figure 9) show that the controller can have five simultaneous connections, but not more than five (the first query has matching states, but the second query does not), as desired.  
Figure 5: The IOPT edition tool with the model of the controller of the NOVA-WiFi-Client Provider (NWCP) module.  
Figure 6: The IOPT simulation tool with the model of the controller of the NOVA-WiFi-Beacon Provider (NWBP) module.  
After model validation through simulations and model-checking, the modules code is automatically generated while using the IOPT C code generator. Using an automatic code generator, it is possible to ensure that the implementation code conforms with the validated model. To generate the implementation code, it is only required to press the C code button that is shown in Figure 10. As previously mentioned (Section 4), the automatic code generator additionally generates an HTTP server that supports the debugger tool.  
Figure 8: IOPT query edition tool with the queries performed to the controller model of the NWBP module.  
Figure 7: State-space of the controller model of the NWBP module.  
Figure 9: Query results of the controller model of the NWBP module.  
The Debugger button from the interface presented in Figure 10 opens the debugger tool. This tool supports not only the system tests (the fifth step of the development approach), but also its remote control and monitoring (implements the RCMSP module) during its normal and maintenance operations. To connect the debugger tool (that has an interface similar to the simulator tool) to each NWB, it is required to introduce its IP address, Port, and password, as presented in Figure 11.