随着互联网和移动终端的发展,基于互联网的社交新媒介不断的出现,人们的社交活动越来越依赖于社交应用。微信是腾讯公司在2011年发布的一款应用,截止到2019年第三季度,微信月活跃账户数已达11.51亿,小程序日活跃账户数超3亿。微信拥有门槛低、实时性高、互动性强等特点,不同阶层和年龄段的人均可以在网上发表自己的见解,并且通过与群友或好友的互动交流迅速地传播信息。但是,有些用户会在微信中发布一些不良信息,影响网络环境的和谐。为了更好的关注社交网络舆情发展和引导社会舆论,了解微信在信息传播上的特点和性质是很有必要的。从软件角度研究微信系统,可以使用软件验证的方式判定其特定性质是否满足。运行时验证相比传统的模型检测、测试和定理证明等软件验证方法,拥有复杂度低、易于操作等特点,适合用于在线验证微信系统的性质。当前对微信系统信息传播的特点和性质进行的研究,主要集中在微信公众平台的热点挖掘和分析等方面,关于微信群的信息传播特征和用户行为的研究比较少。本文提出一种基于三值命题投影时序逻辑（Three-valued Propositional Projection Temporal Logic,PPTL₃）的微信群在线运行时验证方法。首先,分析微信官方发布的协议和社交网络相关的法律法规,得出微信群传播信息时需要满足的性质,并且根据性质定义原子命题,将原子命题组合成描述性质的PPTL₃公式,使用PPTL性质监控器生成器（Property Monitor Generation of PPTL property,PMG_PPTL）得到公式对应的监控器,再使用Java监控器生成器读取保存监控器信息的文本文件,生成Java格式的监控器。其次,使用爬虫程序动态获取微信群的数据,分析需要验证的性质并确定相关的微信文本,使用融合词特征、文本格式特征和文本语义特征的文本分类方法和基于关键词过滤的自动机算法识别特定的微信文本,进而判定原子命题真假值。然后,将原子命题组合成表示系统路径的状态子公式并输入到Java监控器中,如果到达TRUE节点,表明性质成立;如果到达FALSE节点,表明性质不成立;如果到达其他节点,说明当前获取到的信息无法判定性质是否成立,需要继续运行。最后,通过将本方法采用的运行时验证工具和其他工具进行对比,表明了所采用的工具在验证微信群性质上的有效性。