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

Safety design of IoT operating system based on linear temporal logic

作　　者：张华强 李凯航 王继刚 Zhang Huaqiang;Li Kaihang;Wang Jigang(Chengdu R&D Center of ZTE Corporation,Chengdu 610041,China)

机构地区：[1]中兴通讯成都研发中心

出　　处：《电子技术应用》2020年第2期92-97,102,共7页Application of Electronic Technique

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

关 键 词：物联网操作系统 经典现行时态逻辑 形式化模型检测理论 安全性设计 

分 类 号：TN401[电子电信—微电子学与固体电子学] TP311[自动化与计算机技术—计算机软件与理论]