计算机科学 ›› 2009, Vol. 36 ›› Issue (10): 164-167.
王小兵,段振华
WANG Xiao-bing, DUAN Zhen-hua
摘要: 时序逻辑程序的形式化验证对提高程序的正确性具有重要意义。以投影时序逻辑的可执行子集、框架投影时序逻辑语言Framed Tempura为研究对象,使用命题投影时序逻辑描述Framed Tempura程序的性质,将程序h和性质ф统一表示在投影时序逻辑中,模型检测需要判定p→ф是否有效,可转化为判定p∧乛ф是否不可满足,这可以通过构造p∧乛ф的正则图加以解决。最后,给出了Framed Tempura程序的模型检测实例。
No related articles found! |
|