论文部分内容阅读
针对语义物联网服务的正确性验证问题,提出基于时态描述逻辑与命题μ-演算相结合的语义物联网服务验证方法。利用描述逻辑中的ABox对系统模型进行标注,引入语义标注的有限状态机对语义物联网服务进行建模。将描述逻辑ALC与命题μ-演算结合,构建时态描述逻辑ALC-μ,用于待验证性质的刻画。采用模型检测机制与描述逻辑推理机制相结合的模型检测算法,验证语义物联网服务的正确性。该方法可准确地对语义物联网服务进行建模和对所期望性质进行验证,并得到符合该性质的状态集合。