当前位置:主页 > 科技 > 文章内容

鹰潭信息港:基于线性时态逻辑的物联网操纵系统安全性设计

日期:2020-03-14 浏览:

跟着物联网技能的成长,物联网设备安全性问题将是急需办理的焦点问题之一。同时,在保障物联网设备安全的所有法子中操纵系统层面的安全是重中之重,从本质上讲,可以说物联网操纵系统的安全性直接抉择了整个物联网设备系统的靠得住性。

本文在上述配景下提出了一套行之有效的针对物联网操纵系统的安全性设计理论,目标是办理上述焦点问题。

1 操纵系统安全性

传统的操纵系统设计要领主要依赖于人的以往履历和简朴的逻辑阐明,因此无法从基础上担保操纵系统设计的安全性和正确性。

形式化要领的焦点就是形式化语言,以及基于形式化语言构建出来的形式化模子。其基本思路是将高靠得住性系统用语义明晰的形式化语言举办建模,回收模子检测、定理证明的要领对系统方针属性举办正确性推演和验证。因此,回收该要领举办操纵系统的设计和验证可以或许担保操纵系统的安全性和确定性[1-2]。

2 操纵系统形式化设计理论模子

颠末大量的工程实践较量与研究,本文提出了基于线性时态逻辑的操纵系统形式化设计理论模子[2],如图1所示。


鹰潭信息港:基于线性时态逻辑的物联网操纵系统安全性设计

图24所示暗示批改后的时态逻辑已经通过正确性查抄。可以直接利用验证过的数学模子举办方针代码编写和测试。

上述案例说明形式化要领可以从系统设计层面就能担保需求实现的完整性和设计模子的安全性、正确性。

4 竣事语

对付物联网操纵系统的需求观念模子设计与验证利用线性时态逻辑来做是较量高效的选择。利用本文提出的设计要领可以在顶层逻辑措施设计阶段就将需求观念模子举办准确描写,纵然是错误的模子或在求精设计阶段存在BUG,也可以通过期态逻辑的属性验证发明并举办修改优化。利用线性时态逻辑作为顶层逻辑模子的求精既担保了与顶层需求模子的一致性,又担保了求精模子可以在实现层面很容易向方针代码转换。这部门固然只能做到部门形式化,可是只需颠末简朴的方针测试就可以完成产物方针代码最终的验证事情。

本文提出的理论要领对付其他对安全性和靠得住性要求较高的软件设计规模也具有极高的参考代价。

参考文献

[1] LAMPORT L.Specifying systems[M].Boston:Pearson Education,Inc.,2002.

[2] ABELSON H,SUSSMAN G J,SUSSMAN J.Structure and interpretation of computer programs[M].Cambridge,Massachusetts London,England:The MIT Press,1996.

[3] 朱峰,鲁征浩,朱青.形式化验证在处理惩罚器浮点运算单位中的应用[J].电子技能应用,2017,43(2):29-32.

[4] ROSEN K H.离散数学及其应用(原书第七版)[M].徐六通,杨娟,吴斌,译.北京:机器工业出书社,2017.

[5] 张杰,王少超,关永.基于形式化要领的有限域乘法器的建模与验证[J].电子技能应用,2018,44(1):109-113.

[6] Yu Yuan,MANOLIOS P,LAMPORT L.Model checking TLA+ specifications[C].Lecture Notes in Computer Science,Number 1703,Springer-Verlag,1999:54-66.

[7] 贺江,蒲宇亮,李海波,等.一种基于OpenCL的高能效并行KNN算法及其GPU验证[J].电子技能应用,2016,42(2):14-16.

[8] NIPKOW T,PAULSON L C,WENZEL M.高阶逻辑帮助证明系统[M].陈光喜,刘卓军,译.北京:北京理工大学出书社,2013.