（國防科學技術大學計算機學院，長沙 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-） 男，在讀碩士，主要研究領域為高可信軟件技術
