（国防科学技术大学计算机学院，长沙 410073）
摘要：本文结合作者课题内容，对基于JAVA-MOP工具软件添加逻辑库的方法和机制进行了深入的研究，首先，本文详细介绍了JAVA-MOP工具软件，探讨了其采用反射机制调用逻辑库的机理，并对出现的若干问题如多进程的调试等提出了自己的解决方案，最后作者示例如何添加基于线性时序逻辑三值语义监控器生成的ltl3逻辑库。
关键词： JAVA-MOP；逻辑库；反射机制；线性时序逻辑；三值语义；ltl3逻辑库；
参考文献
J.Peleska.Java-MOP_A_monitoring_oriented_programming_environment_for_Java: Third International symposium of Formal Methods Europe. In LNCS, 2012, 1051:39~59.
Aandreas Bauer, Martin Leucker, and Christian Schallhart, Runtime Verification for LTL and TLTL. ACM Transactions on Software Engineering and Methodology, 2009, 1346：8~23.
MaCware. http://fsl.cs.illinois.edu/index.php/Formal_Systems_Laboratory, 2008/2014.
本文直接来源于863计划项目《面向信息-物理融合的系统平台》子课题《CPS系统监控与演化技术》
作者简介：
周戈（1984.10-） 男，在读硕士，主要研究领域为运行时验证技术；
于康（1987.07-） 男，在读博士，主要研究领域为软件工程
徐蛟（1990.01-） 男，在读硕士，主要研究领域为高可信软件技术
