基于线性时态逻辑的物联网操作系统安全性设计

Safety design of IoT operating system based on linear temporal logic

根据物联网操作系统安全性设计的需求,同时结合在经典线性时态逻辑、逻辑程序设计、形式化模型检测理论方面的研究与工程实践探索,提出了一种应用于物联网操作系统安全性设计的方法论,并进行了工程原型验证。实践证明该方法的效果符合预期,不仅适合物联网操作系统的安全性设计,也可以进一步推广到其他安全性要求较高的软件产品设计领域。

In this paper,according to the requirement of safety design of IoT(Internet of Things)operating system,combined with the research and engineering practice of classical linear temporal logic,logic programming and theory of formal model detection,a methodology for safety design of IoT operating system is proposed,and the engineering prototype is validated.Practice has proved that the effect of this method is in line with expectations.It is not only suitable for the safety design of IoT operating system,but also can be further extended to other areas of software product design with high safety requirements.