Do you think we need a systematic approach for formal verification of IoT-enabled nodes? If yes what aspects do you think are necessary to be considered in the verification process?
First of all, yes we definitely need a formal way to verify each IoT-enabled node and it should be something like what was done in [1].
This verification process and features should be part of a bigger and more comprehensive standard that the IoT-enabled devices manufacturers need to agree on.
The aspects that this standard should include can be:
- minimum IoT protocols support (ex. MQTT, HTTP, CoAP, ...etc).
- complying with the minimum security (authentication, authorization, and encryption) requirements.
- durability of the device and its battery lifetime.
and so many other aspects that are application specific.
As a real time system the IOT software can be formally modeled and verified. A simulator is required to generate test data for testing the software. The time constraint and criticality levels should be considered, when testing the software.