Formal Verification of a Hybrid IoT Operating System Model

The Internet of Things (IoT) is becoming an increasingly common paradigm. As IoT usage scenarios have increased, many challenges in IoT operating systems' safety and adaptability have remained. According to the programming model, IoT operating systems can be categorized into three types: multithreading, event-driven, and hybrid. Different operating system models are applied in different scenarios depending on the real-time requirements or resource richness. The safety of IoT operating systems is critical; hence, formal verification is an important method of detecting potential vulnerabilities and providing safety guarantees. This paper proposes a hybrid model for an IoT operating system and employs the Event-B method for modeling and verification. We rewrite the requirements and divide the Event-Bus hybrid operating system model into eight levels for refinement. The safety and liveness properties of Event-Bus are guaranteed by generating and proving the proof obligations at each model level. A large proportion of the proof obligations (91%) are automatically proven on the Rodin platform to simplify the development process.