摘要
本发明公开了一种基于PPTL-3的社交网络系统隐私安全运行时验证方法,对于待验证的性质P,用PPTL-3公式来描述,然后分别将P与非P所对应的逻辑公式转化为范式,并进一步转化为范式图及带标记的范式图,根据后者可求得相应的Buchi自动机,通过改变接受集来定义一个有穷自动机并对其确定化,最终对有穷自动机求积以构造监控器;在此基础上,还公开了运行时验证在社交网络系统中的应用,通过PPTL-3公式来描述社交网络应满足的性质,并建立相应的监控器,在系统运行的时候,对其进行监控以判断当前的运行是否满足该性质。
- 单位