一种运行时验证监控器的构造方法

下载PDF

导出

摘要本文结合作者课题内容,介绍了一种运行时验证技术中的监控器构造方法。该方法完整涵盖了从性质规约到监控器模型再到监控程序的全过程,过程中使用了相关开源的第三方软件使得该方法的自动化程度较高。同时由于该监控器的构造是基于三值语义,使得该监控器在一定意义上具有预测性。

作者张可迪董威

机构地区国防科学技术大学计算机学院

出处《计算机光盘软件与应用》 2012年第20期75-76,共2页 Computer CD Software and Application

关键词运行时验证监控器模型监控程序三值语义

参考文献7

1S.Colin,L.Mariani. Run-Time Verification,chapter 18[J].Lecture Notes in Computer Science,2005.525-555.
2J.Peleska. Test automation for safety-critical systems:Industrial application and future developments[A].1996.39-59.
3E.M.Clarke,O.Grumberg,D.A.Peled. Model Checkin g[J].Lecture Notes in Computer Science,2006.54-56.
4F.Kroger. The temporal logic of programs[M].N ewYork,USA:Springer-Verlag New York,1987.132-143.
5M.Geilen. “On the construction of monitors for temporal logic properties[J].Electronic Notes in Theoretical Computer Science,2001,(02).
6Bauer,A,Leucher,M,Schallhart,C. Runtime verification for LTL and PTLTL.[Technical Report TUM-I0724][R].TU München,2007.
7M.Kim,S.Kannan,I.Lee,O.Sokolsky,M.Viswanathan. Java-MaC:a runtime assurance approach for Java programs[J].Formal Methods in Systems Design,2004,(02):129-155.

计算机光盘软件与应用

2012年第20期

内容加载中请稍等...