基于运行时验证的软件监控关键技术研究
|
摘要
运行时验证是一种轻量级的运行时监控技术。通过持续监控软件系统的运行状态来判定当前系统运行是否满足通过某种高层规约描述的正确性性质。在运行时验证中，通常从高层规约中自动产生运行时监控器。在系统运行过程中，运行时监控器在任何时刻仅能观察到在理想情况下为无穷状态序列的系统执行的有穷前缀。传统的运行时验证技术无法预测被监控软件系统未来可能的执行行为。运行时监控器监控结论的产生仅能依据当前观察的有穷前缀。故仅能检测当前系统执行中的软件失效，而不能预测软件失效的发生。对于部署后软件，及时检测到软件失效固然重要，但预测软件失效并避免其发生更有意义。
本文围绕运行时软件失效预测和预防问题，一方面研究软件系统一般时序性质和参数化时序性质的预测语义和预测监控器构造技术，尽可能早的检测软件失效；另一方面，通过前瞻软件行为把控制和反馈的概念引入软件运行过程，提出了软件主动监控的概念和方法，形成由失效预测和预防形成的闭环回路。使得软件运行时验证及主动监控技术成为传统软件分析和验证技术的有效补充，提高部署后软件系统的安全性、可靠性。
本文首先基于线性时序逻辑预测语义定义，研究和提出了改进的预测监控器构造方法。运行时验证中的一个重要研究内容就是从高层规约生成高效的监控器。本文提出的构造方法使最终产生的预测监控器规模尽可能小，能有效控制构造过程复杂度，避免状态爆炸从而增强该方法的适用性。
以面向线性时序逻辑的运行时验证技术为基础，提出了基于软件系统模型的软件主动监控技术和方法。在系统模型中，不但关心系统状态之间的迁移关系，而且关心驱使状态迁移发生的方法和事件。本文以该模型为基础，提出了如何前瞻系统行为，如何针对运行时监控器监控结论自动产生在特定状态处的调控动作，以及如何采用适当的执行机制使得调控动作能够被及时使能和饨化，从而避免软件失效的方法和技术，形成包含失效预测及预防的闭环回路，使得被监控系统的行为能够向着期望的方向被不断监控和调控。同时本文还证明了，在特定的条件下，主动监控技术总能保证系统的实际运行行为与期望的系统行为之间的一致性。
针对描述程序动态属性的特殊需求，本文进一步研究了面向参数化线性时序性质的运行时验证技术，首先综合考虑运行时验证以及参数化线性时序性质描述两方面的特殊需求，提出了既适于运行时验证技术，又能满足参数化性质描述的参数化线性时序逻辑，即PAⅡL，从语法层面保证公式中参数化变量的绑定和使用等基本操作的实施。同时给出了相应的标准语义和预测语义。以此为基础，提出了以交错自动机为中间环节的单一整体参数化预测监控器构造技术，并通过形式化的方法定义了参数化预测监控器的运行过程。该监控器基于参数化系统执行轨迹能够尽可能早的检测当前系统执行中的软件失效。
由于PAⅡL逻辑强大的表达能力，使得单一整体参数化预测监控产生过程复杂度比较高及理论比较复杂，本文进一步提出了一种表达能力受限的描述参数化线性时序性质的形式化方法，LTL模板。它与一般的线性时序逻辑存在比较紧密的对应关系。因此，本文研究了如何把参数化系统执行轨迹转化为一组非参数化的程序执行轨迹，从而把面向参数化时序性质的运行时验证问题转化为面向一般线性时序性质的验证问题。这就使得上述关于面向LTL的运行时验证和主动监控技术得以在参数化环境应用。
最后，本文以操作系统信息安全访问控制机制为典型应用背景，展示了如何利用上述软件运行时验证和主动在线监控技术和方法框架，在系统运行时过程中，进一步精化sELillLIx操作系统安全策略配置。从而实现进一步提高软件系统信息流安全的目标。验证了本文方法的有效性。
Runtime verification (RV) is a lightweight runtime monitoring technique. It aims to check whether an execution of a system under scrutiny satisfies or violates a given correctness property expressed as some types of top-level specification through observing its running continuously. In runtime verification, a correctness property is typically automatically translated into a monitor. During runtime, at any time the monitor can just observe a finite prefix of an execution which should be an infinite states sequence in ideal situation. For traditional techniques of RV, because they are not concerned with and can not look-ahead the future behaviors of the system under scrutiny, the verdicts of monitors are given just on the basis of the current observed finite prefix. Thus, the traditional techniques of RV can just detect the occurrence of failure, but can not predict possible faults in advance effectively. In fact, for deployed software, although it is important to detect the occurrence of failure, it is much more meaningful to predict the fault in advance and prevent it from occurring.
In this paper, around the problem on failure prediction and preventention, on one hand, Anticiparoty semantics definition and anticipatory monitor construction for common temporal properties and parameterized temporal properties are reaserched which make failure detection as early as possible. On the other hand, the definitions of control and feedback are imported through looking ahead the future behavior of the system, the definition and method of software active monitoring are proposed. Thus, a closed-loop system is formed which is consisted of prediction and preventention. It’s our purpose to make them to be complementation of other traditional analysis and verification techniques and improve the safety and reliability of deployed software system.
Based on anticipatory semantics of linear temporal logic (LTL), this paper presents an improved construction method of anticipatory monitor. An important aspect in RV is that of synthesizing efficient monitor from specification. The proposed method in this paper is not only making the size of the final anticipatory monitor as small as possible, but also controlling the complexity of intermediate steps to prevent the construction process from being affected due to states explosion and improve applicability of the method.
On the basis of proposed technique of runtime verification for LTL, this paper presents the technique and method of software active monitoring based on system models. In the model, not only the transitions between states are concerned, but also the methods and events which make the transitions happen are considered. Through the model, the paper presents a series of methods and techniques about how to look-ahead the future behaviors of the system, how to generate the corresponding steering actions connected to given state automatically based on the verdicts of monitors and how to enable and disable the actions in time to prevent the failure from occurring through special execution mechanism. At last, a closed-loop containing failure predication and prevention is generated to control the behaviors of observed system towards desired direction through continuously monitoring and steering. Meanwhile, it is proved that under given condition, active monitoring technique always assure the consistency between the actual execution and expected behaviors of the system.
In order to verify the dynamic property, this paper presents RV technique for parameterized linear temporal property further. Based on the consideration about the special requirement of RV itself and the expression of parameterized property, a parameterized linear temporal logic, i.e. PALTL, is proposed which is not only suitable for RV, but also satisfied with the need to describe the parameterized property. It assures that several basic operations such as variables binding and using can be implemented in syntax level. Then, the standard and anticipatory semantics are presented. On the above basis, the paper presents the construction process of a monolithic parameterized anticipatory monitor, and gives the definition of running of the parameterized monitor in formal method. The monitor can detect the failure of current execution based on a parameterized prefix as early as possible.
Due to the strong expressiveness of PALTL, it makes the construction process and theory of monolithic monitor is complicated. This paper presents another constrained formal method to describe parameterized linear temporal properties, i.e. LTL Schema. It has close correspondence with LTL. It has explained how to separate a parameterized trace into several non-parametric sub-traces and how to transfer the problem of RV for parametrized temporal properties to the easier verification problem for a corresponding LTL formula on several non-parametric state traces. It makes the techniques about RV and active monitoring can be applied in parametric context.
Finally, in the context of access control mechanism for security of operating system, it is showed that based on the technique and framework of RV and active monitoring, the security policy configuration of SELinux can be further refined to improve the security information flow goal during runtime. The effectiveness of the proposed method is verified.
本文围绕运行时软件失效预测和预防问题，一方面研究软件系统一般时序性质和参数化时序性质的预测语义和预测监控器构造技术，尽可能早的检测软件失效；另一方面，通过前瞻软件行为把控制和反馈的概念引入软件运行过程，提出了软件主动监控的概念和方法，形成由失效预测和预防形成的闭环回路。使得软件运行时验证及主动监控技术成为传统软件分析和验证技术的有效补充，提高部署后软件系统的安全性、可靠性。
本文首先基于线性时序逻辑预测语义定义，研究和提出了改进的预测监控器构造方法。运行时验证中的一个重要研究内容就是从高层规约生成高效的监控器。本文提出的构造方法使最终产生的预测监控器规模尽可能小，能有效控制构造过程复杂度，避免状态爆炸从而增强该方法的适用性。
以面向线性时序逻辑的运行时验证技术为基础，提出了基于软件系统模型的软件主动监控技术和方法。在系统模型中，不但关心系统状态之间的迁移关系，而且关心驱使状态迁移发生的方法和事件。本文以该模型为基础，提出了如何前瞻系统行为，如何针对运行时监控器监控结论自动产生在特定状态处的调控动作，以及如何采用适当的执行机制使得调控动作能够被及时使能和饨化，从而避免软件失效的方法和技术，形成包含失效预测及预防的闭环回路，使得被监控系统的行为能够向着期望的方向被不断监控和调控。同时本文还证明了，在特定的条件下，主动监控技术总能保证系统的实际运行行为与期望的系统行为之间的一致性。
针对描述程序动态属性的特殊需求，本文进一步研究了面向参数化线性时序性质的运行时验证技术，首先综合考虑运行时验证以及参数化线性时序性质描述两方面的特殊需求，提出了既适于运行时验证技术，又能满足参数化性质描述的参数化线性时序逻辑，即PAⅡL，从语法层面保证公式中参数化变量的绑定和使用等基本操作的实施。同时给出了相应的标准语义和预测语义。以此为基础，提出了以交错自动机为中间环节的单一整体参数化预测监控器构造技术，并通过形式化的方法定义了参数化预测监控器的运行过程。该监控器基于参数化系统执行轨迹能够尽可能早的检测当前系统执行中的软件失效。
由于PAⅡL逻辑强大的表达能力，使得单一整体参数化预测监控产生过程复杂度比较高及理论比较复杂，本文进一步提出了一种表达能力受限的描述参数化线性时序性质的形式化方法，LTL模板。它与一般的线性时序逻辑存在比较紧密的对应关系。因此，本文研究了如何把参数化系统执行轨迹转化为一组非参数化的程序执行轨迹，从而把面向参数化时序性质的运行时验证问题转化为面向一般线性时序性质的验证问题。这就使得上述关于面向LTL的运行时验证和主动监控技术得以在参数化环境应用。
最后，本文以操作系统信息安全访问控制机制为典型应用背景，展示了如何利用上述软件运行时验证和主动在线监控技术和方法框架，在系统运行时过程中，进一步精化sELillLIx操作系统安全策略配置。从而实现进一步提高软件系统信息流安全的目标。验证了本文方法的有效性。
Runtime verification (RV) is a lightweight runtime monitoring technique. It aims to check whether an execution of a system under scrutiny satisfies or violates a given correctness property expressed as some types of top-level specification through observing its running continuously. In runtime verification, a correctness property is typically automatically translated into a monitor. During runtime, at any time the monitor can just observe a finite prefix of an execution which should be an infinite states sequence in ideal situation. For traditional techniques of RV, because they are not concerned with and can not look-ahead the future behaviors of the system under scrutiny, the verdicts of monitors are given just on the basis of the current observed finite prefix. Thus, the traditional techniques of RV can just detect the occurrence of failure, but can not predict possible faults in advance effectively. In fact, for deployed software, although it is important to detect the occurrence of failure, it is much more meaningful to predict the fault in advance and prevent it from occurring.
In this paper, around the problem on failure prediction and preventention, on one hand, Anticiparoty semantics definition and anticipatory monitor construction for common temporal properties and parameterized temporal properties are reaserched which make failure detection as early as possible. On the other hand, the definitions of control and feedback are imported through looking ahead the future behavior of the system, the definition and method of software active monitoring are proposed. Thus, a closed-loop system is formed which is consisted of prediction and preventention. It’s our purpose to make them to be complementation of other traditional analysis and verification techniques and improve the safety and reliability of deployed software system.
Based on anticipatory semantics of linear temporal logic (LTL), this paper presents an improved construction method of anticipatory monitor. An important aspect in RV is that of synthesizing efficient monitor from specification. The proposed method in this paper is not only making the size of the final anticipatory monitor as small as possible, but also controlling the complexity of intermediate steps to prevent the construction process from being affected due to states explosion and improve applicability of the method.
On the basis of proposed technique of runtime verification for LTL, this paper presents the technique and method of software active monitoring based on system models. In the model, not only the transitions between states are concerned, but also the methods and events which make the transitions happen are considered. Through the model, the paper presents a series of methods and techniques about how to look-ahead the future behaviors of the system, how to generate the corresponding steering actions connected to given state automatically based on the verdicts of monitors and how to enable and disable the actions in time to prevent the failure from occurring through special execution mechanism. At last, a closed-loop containing failure predication and prevention is generated to control the behaviors of observed system towards desired direction through continuously monitoring and steering. Meanwhile, it is proved that under given condition, active monitoring technique always assure the consistency between the actual execution and expected behaviors of the system.
In order to verify the dynamic property, this paper presents RV technique for parameterized linear temporal property further. Based on the consideration about the special requirement of RV itself and the expression of parameterized property, a parameterized linear temporal logic, i.e. PALTL, is proposed which is not only suitable for RV, but also satisfied with the need to describe the parameterized property. It assures that several basic operations such as variables binding and using can be implemented in syntax level. Then, the standard and anticipatory semantics are presented. On the above basis, the paper presents the construction process of a monolithic parameterized anticipatory monitor, and gives the definition of running of the parameterized monitor in formal method. The monitor can detect the failure of current execution based on a parameterized prefix as early as possible.
Due to the strong expressiveness of PALTL, it makes the construction process and theory of monolithic monitor is complicated. This paper presents another constrained formal method to describe parameterized linear temporal properties, i.e. LTL Schema. It has close correspondence with LTL. It has explained how to separate a parameterized trace into several non-parametric sub-traces and how to transfer the problem of RV for parametrized temporal properties to the easier verification problem for a corresponding LTL formula on several non-parametric state traces. It makes the techniques about RV and active monitoring can be applied in parametric context.
Finally, in the context of access control mechanism for security of operating system, it is showed that based on the technique and framework of RV and active monitoring, the security policy configuration of SELinux can be further refined to improve the security information flow goal during runtime. The effectiveness of the proposed method is verified.
引文
[1] Clarke，E M，Grumberg，O and Peled，D A Model Checking[M] Massachuse~s：The MIT Press，1999
[2] Alur，R，Courcoubetis，C，Dill，D L Model-checking in dense real-time[Jll Information and Computation，104(1)：2-34
[3] Gabbay，D M，Hogger,C J，Robinson，J A and Siekmann，J H Handbook of Logic in Artificial Intelligence and Logic Programming，Volume2，Deduction Methodologies[M]，London：Oxford University Press，1994
[4]Broy，M Software technology-rmal methods and scientific foundations[J] Information and Software Technology,1999(41)：947-950
[5] Broy，M，Jonsson，B，Katoen，J P，Leucker,M and Pretschner，A Model-based Testing of Reactive Systems，Advanced Lectures[Jl，Lecture Notes in Computer Science，2005(3472)
[6]DaM，O J，Dijkstra，E W and Hoare，C A R Structured Programming[M] London：Academic Press，1972
[7] Biere，A，Cimatti，A，Clarke，E M，Strichman，O and Zhu，Y Bounded model checking[Jll Advances in Computers，Academic Press，2003，Vol 58：118-149
[8] Biere，A，Cimatth，A Clark，E M and Zhu，Y Symbolic model checking without BDDs[Jll Lecture Notes in Computer Science，1999，Vol 1579：193-207
[9] IEEE Std 1012-2004，IEEE standard for software verification and validation[s]，2005，pages 1-110
[10]Hakansson，J，Jonsson，B and Lundqvist，O Generating online test oracles from temporal logic specifications[Jll Journal on Software Tools for Technology Transfer(STTT)，2003，4(4)：456-471[1 1]Kopetz，H Event-triggered versus time-triggered real-time systems[Jll Lecture Notes in Computer Science，1999，vol 563：87-101
[12]Bertot，Y，Cast6ran，P Interactive Theorem Proving and Program Development Coq’Art：The calculus of Inductive Constructions[M]An EATCS Series，2004
[13]Sistla，A P，Clarke，E M Complexity of propositional temporal logics[J] Journal ofthe ACM(JACM)，1985，32：733-749
[14]Myers，G J，Badgett，T，Thomas，T M and Sandier，C The Art of Software Testing[M]John Wiley and Sons，2 edition，2004
[15]Pretschner，A and Leucker，M Model-Based Testing A Glossary[Jll Lecture Notes in Computer Science，2005，v013472：257-279
[16]Christos G Cassandras and Stephane Lafortune Introduction to Discrete-Event System[M]2005
[17]Osterweil，L Software processes are software too[c]In proceedings of the 9thInternational Conference on Software Engineering, Los Alamitos: IEEE Computer Society press,1987:2-13.
[18] Kai-Yuan Cai, Joao W. Cangussu, Ray A. Decarlo, Aditya P. Mathur. An Overview of Software cybernetics [C]. In Proceedings of the Eleventh Annual International Workshop on Software Technology and Engineering Pratice, Washington: IEEE Computer Society Press, 2003: 77-86.
[19] Introduction to SDL 88. http://www.sdl.forum.org/sdl88tutorial/index. html, 2002.
[20] Marchand, H. and Samaan, M. Incremented design of a power transformer station controller using a controller synthesis methodology [J]. IEEE Transactions on Software Engineering, 2000, 26(8):729-741.
[21] X.Y. Wang, Y.C.Li and K.Y.Cai. On the polynomial dynamical system approach to software development [J]. Science in China (Series F), 2004, 47(4): 437-457.
[22] Baskar Sridharan, Aditya P. Mathur and Kai-Yuan Cai. Synthesizing distributed controller for safe operation of connected spaces [C]. In proceedings of the IEEE International Conference on Pervasive Computing and Communication, IEEE Computer Society Press, 2003: 452-459.
[23] Baskar Sridharan, Aditya P. Mathur and Kai-Yuan Cai. Using supervisory control to synthesize safety controllers for connectedspaces [C]. In Proceedings of the 3rd International Conference on Quality Software. IEEE Computer Society Press, 2003: 186-193.
[24] Joao, W. Cangussa, Raymond, A. D. and Aditya, P. M. Using sensitivity to validate a state variable model of the software test process [J]. IEEE Transactions on Software Engineering, 2003, 29(5): 430-443.
[25] Joao, W. Cangussu, Raymond, A. Decarlo and Aditya, P. M. A formal model of the software test process [J]. IEEE Transactions on Software Engineering, 2002, 28(8):782-796.
[26] Dellarocas, C., Klein, M. and Shrobe, H. An architecture for constructing self-evolving software systems [C]. In Proc. of the Third International Software Architecture Workshop, New York: ACM Press, 1998: 29-32.
[27] Bauer, A., Leucker, M. and Schallhart, C. Comparing LTL semantics for runtime verification [J]. Journal of Logic and Computation, 2010, 20(3):651-674.
[28] P. Oreizy et al. An architecture-based approach to self-adaptive software [J]. IEEE Intelligent Systems and their Application, 1999,14(2):54-62.
[29] Eisner, C., Fisman, D., Havlicek, J., Lustig, Y., McIsaac, A. Reasoning with temporal logic on truncated paths [C]. In Proceedings of the 15th International Conference on Computer Aided Verification (CAV’03), ACM Press, 2003: 27-39.
[30] Kamp, H. W. Tense Logic and the Theory of Linear Order [D]. Los Angeles: University of California, 1986.
[31] Andreas Bauer. Model-based runtime verification of distributed reactive systems[D]Munchen：TU Munchen，2007
[32]Bauer，A，Leucker，M and Schallhaxt，C Monitoring of reaRime properties[C] In Proceedings of Foundations of Software Technology and Theoretical Computer Science(FSTTCS’06)，Berlin：Springer-Verlag，2006：260-272
[33]Bauer，A，Leucker，M and Schallhart，C The good，the bad，and the ugly-ut how ugly is ugly?Technical Report TUM-10803[R]Munchen：TU Munchen，2008
[34]Martin Leucker and Christian Schallhaxt A brief account of mntime verification [Jll Journal of Logic and Algebraic Programming，2009，78(5)：293-303
[35]Bauer，A，Leucker，M and Schallhart，C The good，the bad，and the ugly-ut how ugly is ugly?[c]In Proceedings of the 7th International Workshop on Runtime Verification(RV’07)，Berlin：IEEE Society Press，2007：126-138
[36]Havelnnd，K Using runtime analysis to guide model checking ofjava programs [c]In Proceedings of the 7th International SPIN Workshop on SPIN Model Checking and Software Verification London，UK：Springer-Verlag，2000：245．264
[37]Havelund，K and Rosu，G Monitoring Java Programs with Java PathExplorer[Jll Electronic Notes in Theoretical Computer Science，2001，55(2)：97-1 14
[38]Havelund，K and Rosu，G Monitoring programs using rewriting[c]In ASE’01：Proceedings of the 16th IEEE International Conference on Automated Software Engineering Washington：IEEE Computer Society，2001：135-143
[39]Havelund，K and Rosu，G Synthesizing Monitors for Safety Properties[c]In Tools and Algorithms for Construction and Analysis of Systems，Springer Press，2002：342．356
[40]Havelund，K and Rosu，G Efficient Monitoring of Safety Properties Journal on Software Tools for Technology Transfer[Jll 2004，6(2)：1 58-173
[41]Clavel，M，Duran，F，Eker，S，Lincoln，P，Marti-Oliet，N Meseguer，J and Talcott，C The maude 2 0 system[C]In Proceedings of the 14th International Conference on Rewriting Techniques and Applications(RTA 2003)，Berlin：Springer-Verlag，2003：76-87
[42]Rosu，G and Bensalem，S Allen Linear(interval)temporal logic-translation to LTL and monitor synthesis[C]In International Conference on Computer Aided Verification(CAV)，Lecture Notes in Computer Science，2006，vol 4144：263-277
[43]Sen，K and Rosu，G Generating optimal monitors for extended regular expressions[Jll Electronic Notes in Theoretical Computer Science(ENTCS) 2003，89(2)：123-134
[44]Emersion，E A and Clarke，E M Characterizing correctness properties of parallel programs using fixpoints[c]In Proceedings of the 7th Colloquium onAutomata，Languages and Programming London：Springer-Verlag press，1980：169．181
[45]Kristoffersen，K J，Pedersen，C and Andersen，H R Runtime verification of timed LTL using disjunctive normalized equ~ion systems[J]Electronic Notes in Theoretical Computer Science，2003，89(2)2 10-225
[46]Bauer，A，Leucker，M and Schallhaact，C Model-based methods for the runtime analysis of reactive distributed systems[C]In Proceedings of the Australian Software Engineering Conference(ASWEC’06)IEEE Press，2006：243-252
[47]Chen，F and Rosu，G MOP：An Efficient and Generic Runtime Verification Framework[C]In Proceedings of the 22nd Annual ACM SIGPLAN Conference on Object-Oriented Programming，Systems，Languages and Applications (OOPSLA’07)，ACM Press，2007：569-588
[48]Chen，F and Rosu，G Towards monitoring-oriented programming：A paradigm combining specification and implementation[Jl Electronic Notes in Theoretical Computer Science(ENTCS)，2003，89(2)146-161
[49]Giannakopoulou，D and Havelund，K Runtime analysis of linear temporal logic specification[Rl，Tech Rep 01 21，RIACS／USRA 2001
[50]Stolz，V and Bodden，E Temporal assertions using AspectJ[Jll Electronic Notes in Theoretical Computer Science(ENTCS)，2006，144(4)：109-124[5 1]Finkbeiner，B and Sipma，H Checking finite traces using aRemaing automata[Jl Formal Methods in System Design，2003，24(2)：101-127
[52]D’A1Tlorim，M and Rosu，G Efficient monitoring of omega-languages[Jll In Intemational Conference on Computer Aided Verification(CAV)Lecture Notes in Computer Science，2007，vol 3576：364-378
[53]Dong W，Leucker M，SchalNart C Impartial anticipation in runtime verification [C]In Proc ofthe 6th Int’1 Symp on Automated Technology for Verification and Analysis(ATVA 2008)Heidelberg：Springer-Verlag，2008：386-396
[54]Sen，K and Rosu，G Generating optimal monRors for extended regular expressions [Jll Electronic Notes in Theoretical Computer Science (ENTCS)，2003，89(2)
[55]Martin，M C，Livshits，V B and Lam，M S Finding application errors and security flaw-s using PQL：a program query language[c]In Conference on Object-Oriented Programming，Systems，Languages，and Applications(OOPSLA)，New-York：ACM Press，2005：365-383
[56]Barringer，H，Goldberg，A，Havelund，K and Sen，K Program monitoring with LTL in Eagle[C]In Intemational Conference of Parallel and Distributed Processing Symposium(IPDPS)，New-Mexico：IEEE Society Press，2004
[57]Chris Allan，Pavel Avgustinov，Aske Simon Christensen，Laurie Hendren，Sasche Kuzins，Ondrej Lhotak,Oege de Moor，DaJnien Sereni，Ganesh Sittaanpalam，andJulian Tibble Adding trace matching with free variables to aspectJ In Proceedings of the 20th annual ACM SIGPLAN conference on Object-oriented programming，systems，languages，and applications，New-York：ACM Press，2005：345．364
[58]Pavel Avgustinov，Julian Tibble and Oege de Moor Making trace monitors feasible[Jll SIGPLAN，2007，42(10)：589-608
[59]Patrick Meredith，Dongyun Jin，Feng Chen and Grigore Rosu Efficient monitoring of parametric context-free patterns[Jll In Journal of Antomated Software Engineering，2010，17(2)：149-180
[60]Eric Bodden Efficient and Expressive Runtime Verification for Java[c]In Proceedings of the Grand finals of the ACM Student Research Competition，San Francisco：ACM Press，2005：123-134
[61]Barringer，H，Rydeheard，D E and Havelund，K Rule systems for run-time monitoring：From eagle to ruler[Jll Lecture Notes in Computer Science，2007，vol 4839：111．125
[62]D’Angelo，B，Sankaacanarayanan，S，Sanchez，C，Robinson，W，Finkbeiner，B，Sipma，H B，Mehrotra,S and Manna，Z LOLA：Runtime monitoring of synchronous systems [C] In International Symposium on Temporal Representation and Reasoning(TIME)ACM Press，2005：166-174
[63]Kim，M，Viswanathan，M，Kannan，S，Lee，I and Sokolsky，O Java-mac：A runtime assurance approach for java programs[Jll Formal Methods in System Design(FMSD)，2004，24(2)：129-1 55
[64]Kim，M，Kannan，S，Lee，I，Sokolsky，O and Viswanathan，M Computational analysis of run-time monitoring fundamentals ofjava-mac[Jll Electronic Notes in Theoretical Computer Science(ENTCS)，2004，70(4)：136-145
[65]Moonjoo，Kim Insup Lee，Usa Sammapun，Jangwoo Shin，Oleg Sokolsky Monitoring，Checking，and steering of Real-time Systems[c]In Proceedings of 2nd International Workshop on Runtime Verification，ENTCS，2002
[66]Moonjoo，Kim Insup Lee，Steering of Real-time Systems Based on Monitoring and Checking[C]In Proceedings of the Fifth International Workshop on Object-Oriented Real-time Dependable Systems，Washington：IEEE Computer Society,1999：1 1-21
[67]Oleg Sokolsky,Usa Sammapun，Insup Lee，Jesung Kim Run-time checking of Dynamic Properties[c]In Proceedings of Electr Notes Theor Comput Sci，IEEE Society Press，2006：91-108
[68]Rabin,M O and Scott，D Finite automata and thek decision problems[J]IBM Journal ofResearch and Development，1959，3：115-125
[69]Meyer，A R and Fischer，M J Economy of description by automata grammars，and formal systems[C]In Proc 12th IEEE Symp On Switching and AutomataTheory,IEEE Society Press，1971：188-191
[70]Sistla，A P and Clarke，E M Complexity of propositional temporal logics[Jll Journal ofthe ACM(JACM)，1985，32(3)：733-749
[71]B~chi，J R On a decision method in restricted second order arithmetic[c]In Proc Intemational Conference on Logic，Method and Philosophe，Stanford：Stanford University Press，1962：1-12
[72]Sistla，A P，Vaacdi,M Y and Wolper，P The complementation problem for B~chi automata with applications to temporal logic[Jll Theoretical Computer Science，1987，49：217-237
[73]Safra，S On the complexity of omega-automata[C]In Proceedings of the 29th Annual Symposium on Foundations of Computer Science，FoCS’88，Los Alamitos：IEEE Computer Society Press，1988：3 19-327
[74]Alpern，B and Schneider，F B[c]Recognizing safety and liveness Distributed Computing，1987，2(3)：1 17-126
[75]Brzozowski，J A and Leiss，E Finite automata and sequential networks[Jll Theoretical Computer Science，1980，10：19-35
[76]Chandra，A K，Kozen，D C and Stockmeyer，L J Alternation[Jll Journal of the Association for Computing Machinery,1981，28(1)：1 14-133
[77]Emst Leiss Succinct representation ofregular languages by Boolean automata[c] Theorectical Computer Science，1981，38(13)：323-330
[78]Muller，D E and Schupp，P E Alternating automata on infinite trees[Jll Theoretical Computer Science，1987，54：267-276
[79]Miyano，S and Hayashi，T Alternating finite automata on f11-words[Jll Theoretical Computer Science，1984，32：321-330
[80]Pnueli，A The temporal logic of programs[c]In Proceedings of the 1 8th IEEE Symposium on the Foundations of Computer Science(FOCS’77)Providence：IEEE Computer Society Press，1977：125-137
[81]Thomas，W Automata on infinite objects[Jll In Handbook of Theoretical Computer Science，vol B，chap 4 Elsevier Science Publishers B V，133-191
[82]Lamport，L What good is temporal logic?[c]In Proceedings of the IFIP 9th World Computer Congress，IEEE Society Press，1983：657-668
[83]Pnueli，A Application of temporal logic to the specification and verification of reactive systems：a survey of current trends[c]In Current trends in concurrency Overviews and tutorials，New-York：Springer-Verlag，1986：510-584
[84]Dwyer，M B，Avrunin，G S and Corbett，J C Patterns in Prope~y Specification for nnite-state verification[C]In Intemational Conference on Software Engineering(IcsE)New-York：ACM Press，1999：41 1-420
[85]Baresi，L，Guinea，S and Pasquale，L Towards a unified framework for themonitoring and recovery of bpel processes．In Proceedings of TAV-WEB．New- York：ACM，2008：15-19
[86]Muller，D E Saoudi，A and Schupp，P E Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential time[c]In Proceedings of 3rd IEEE Symposium on Logic in Computer Science，Edinburgh：IEEE Press，1988：422-427
[87]Barbon，F，Traverso，P，Pistore，M and Trainotti，M Run-time monitoring of instances and classes of web service compositions[c] In International Conference on Web Services(ICWS)Washington：IEEE Computer Society, 2006：63．71
[88]Vaxdi，M Y Nontraditional applications of automata theory[Jll Lecture Notes in Computer Science，1994，volume 789：575-597
[89]Vardi，M Y and Wolper，P Reasoning about infinite computations[Jll Information and Computation，1994，1 15(1)：1-37
[90]Kupferman,O and Vardi，M Y Model Checking of Safety Properties[Jl Formal Methods in System Design(FMSD)，2001，19(3)：291-314
[91]Geilen，M On the Construction of monitors for temporal logic properties[Jll In Electronic Notes in Theoretical Computer Science，2001，55(2)：181-199
[92]Bauer A，Leucher M，Schallhaxt C Runtime verification for LTL and PTLTL[R] Technical Report，TUM-10724，Mfinchen：TU Mfinchen，2007
[93]Vaxdi，M Y，Wolper，P An automata-theoretic approach to automatic program verification[c]In Proceedings of Logic in Computer Science(LICS)，1986：332．345
[94]Corber,J Dwyer，M，Hatclifl．J，Pasareamu，C，Laubach，S and Zheng，H Bandera：Extracting fmite-state models from java source code[c]In proceedings of the 22nd International Conference on Software Engineering(IcsE)，2000：439．448
[95]Havelund，K and Pressburger，T Model checking java programs using Java PathFinder[Jll International Journal on Software Tools for Technology Transfer，2000，2(4)：366-381
[96]Feather，M S，Fickas，S，Van Lamsweerde，A and Pondard，C Reconciling system requirements and runtime behavior[C]In 9th International Workshop on Software Specification and Design，New-York：IEEE Computer Society，1998：50．59
[97]Arvind Easwaran，Sampath Kannan，and Oleg Sokolsky Steering of discrete event systems：control theory approach[Jll In Electronic Notes in Theoretical Computer Science，2005，144(4)：21-39
[98]Schwoon，S and Espaxza，J A note on on-the-fly verification algorithms[Jl In tools and Algorithms for the construction and analysis of Systems(TACAS)Lecture Notes in Computer Science，2006 vol 3440：174。190
[99]Feng chen，Choonghwan Lee，Grigore rosu Mining parametric specifications[R] Illinois：University of Illinois，20 10
[100]Choonghwan Lee，Feng Chen，Grigore Rosu Mining parametric specifications [C]In Proceedings ofthe 30th International Conference on Software Engineering，2011
[101]Hao Chen，David Wagner MOPS：an Infrastructure for Examining Secur~y Properties of Software In Proceedings of ACM Conference on Computer and Communications Secur~y，Chicago：ACM Press，1993：109-121
[102]Patrick O’Neil Meredith，Dongyun Jin，Dennis Griffith，Feng Chen，Grigore Rosu An overview ofthe mop runtime verification framework[c]，Springer，20 1 1
[103]Sheng-Luen Chung，Stephane Lafortune，and Feng Lin Limited lookaJaead policies in supervisory control of discrete event systems[Jll In IEEE Transactions on Automatic Control，1992，Volume 37：(18-31)
[104]Sheng-Luen Chung，Stephane Lafortune，and Feng Lin Supervisory control using variable lookahead policies[c]In Proceedings of Discrete Event Systems Kluw-er．1994
[105]Kim，M，Viswanathan，M，S K Haaaene Ben-Abdallah，Lee，I and Sokolsky，O Formally specified monitoring of temporal properties[c]In proceedings of European Conference on Real-time Systems，1999
[106]Stolz，V Temporal assertions with paacameterized propositions[Jll Journal of Logic and Computation，2008
[107]Stolz，V Temporal assertions for sequential and concurrent programs[D]，Aachen：RWTH University，2007：176-187
[108]Stolz V and Bodden，E Temporal Assertions using AspectJ[c]In Proceedings offifth workshop on Runtime verification(RV’05)，2005：201-216
[109]Stolz，V and Huch，F Runtime Verification of Concurrent Haskell Programs[J] Electronic Notes in Theoretical Computer Science(ENTCS)，2005，1 13：201-216
[110]Va*di MY An automata-theoretic approach to linear temporal logic[C]In Proc of the Logics for Concurrency：Structure Versus Automata,New-York：Springer-Verlag，1996：238266
[111]Java Technology Center，Compaq Corp Compaq JTrek Online documentation：http：／／www digital com／java／download／jtrek／2008
[112]Bauer，A，Leucker，M and Schallhart，C Runtime verification for LTL andTuL[Jll ACM Transactions on Software Engineering and Methodology(TOSEM)，20 10 In press
[113]Feng Chen and Grigore Rosu Parametric trace slicing and monitoring In TACAS，volume 5505 of Lecture Notes in Computer Science，Springer Press，2009：246-261
[114]Grigore Rosu and Feng Chen Parametric Trace Slicing and Monitoring[Rl，Technical Report，UIUCDCS-R-2008-2977，Illinois：University of Illinois，2008
[115]Memcheck,http：／／valgrind org 2007
[116]Loscocco，P A，Smalley，s D，Muckelbauer，P A，Taylor，R C，Turner，s J and Farrell，J F The inevitability offailure：The flawed assumption of security in modern computing environments[c]In Proceedings of the 21st National Information Systems Security Conference，New-York：IEEE Society Press，1998：303．314
[117]Abrams，M D，Jajodia,S，Podell，H J Information Security：An Integrated Collection ofEssays[Rl，IEEE Comp 1995
[118]Lepreau，J The Persistent Relevance of the Local Operating System to Global Applications[c]In Proceedings of the 7th ACM SIGOPS European Workshop，1996
[119]Andrei SabeHbld and Andrew-C Myers Language-based information-flow- security[Jl IEEE Journal on Selected Areas in Communication，2003，21(1)：5-19
[120]Herzog，A and Guttman，J Achieving security goals with Security-Enhanced Linux[Rl，Tech rep，Mitre Corporation，2002
[121]Joshua D Guttman，Amy L Herzog，John D Ramsdell，Clement W Skorupka Verifying information flow-goals in Security-Enhanced Linux[Jll Journal of Computer Security，2005，13(1)：115-134
[122]Changzhi Zhao，Wei Dong，Zhichang Qi Active Monitoring for Control Systems under Anticipatory Semantics[c] In proceedings of 10th International Conference on Quality Software，Zhangjiajie：IEEE CPS，2010：318-325
[123]Chaaagzhi Zhao，Wei Dong，Ji Wang，Ping Sui and Zhichang Qi Software Active Online Monitoring Under Anticipatory Semantics[C]In Proceedings of 1st International Workshop on Software Health Management Online Published at http：／／www isis vanderbiR-edu／workshops／smc-it-2009-shm／，2009
[124]Randal E Bryant Graph-Based Algorithms for Boolean Function Maniputation l Jl Journal ofIEEE Transactions on Computers，1986，35：677-691
[125]A W Roscoe alad M H Goldsmith What is intransitive noninterference?[c]In Proceedings of 12th IEEE Computer Security Foundation Workshop 2003
[126]SLAT：SELinux policy file analysis tool http：／／www dsi unive it／- IFIPWGl 7Vits2003 html 2004
[2] Alur，R，Courcoubetis，C，Dill，D L Model-checking in dense real-time[Jll Information and Computation，104(1)：2-34
[3] Gabbay，D M，Hogger,C J，Robinson，J A and Siekmann，J H Handbook of Logic in Artificial Intelligence and Logic Programming，Volume2，Deduction Methodologies[M]，London：Oxford University Press，1994
[4]Broy，M Software technology-rmal methods and scientific foundations[J] Information and Software Technology,1999(41)：947-950
[5] Broy，M，Jonsson，B，Katoen，J P，Leucker,M and Pretschner，A Model-based Testing of Reactive Systems，Advanced Lectures[Jl，Lecture Notes in Computer Science，2005(3472)
[6]DaM，O J，Dijkstra，E W and Hoare，C A R Structured Programming[M] London：Academic Press，1972
[7] Biere，A，Cimatti，A，Clarke，E M，Strichman，O and Zhu，Y Bounded model checking[Jll Advances in Computers，Academic Press，2003，Vol 58：118-149
[8] Biere，A，Cimatth，A Clark，E M and Zhu，Y Symbolic model checking without BDDs[Jll Lecture Notes in Computer Science，1999，Vol 1579：193-207
[9] IEEE Std 1012-2004，IEEE standard for software verification and validation[s]，2005，pages 1-110
[10]Hakansson，J，Jonsson，B and Lundqvist，O Generating online test oracles from temporal logic specifications[Jll Journal on Software Tools for Technology Transfer(STTT)，2003，4(4)：456-471[1 1]Kopetz，H Event-triggered versus time-triggered real-time systems[Jll Lecture Notes in Computer Science，1999，vol 563：87-101
[12]Bertot，Y，Cast6ran，P Interactive Theorem Proving and Program Development Coq’Art：The calculus of Inductive Constructions[M]An EATCS Series，2004
[13]Sistla，A P，Clarke，E M Complexity of propositional temporal logics[J] Journal ofthe ACM(JACM)，1985，32：733-749
[14]Myers，G J，Badgett，T，Thomas，T M and Sandier，C The Art of Software Testing[M]John Wiley and Sons，2 edition，2004
[15]Pretschner，A and Leucker，M Model-Based Testing A Glossary[Jll Lecture Notes in Computer Science，2005，v013472：257-279
[16]Christos G Cassandras and Stephane Lafortune Introduction to Discrete-Event System[M]2005
[17]Osterweil，L Software processes are software too[c]In proceedings of the 9thInternational Conference on Software Engineering, Los Alamitos: IEEE Computer Society press,1987:2-13.
[18] Kai-Yuan Cai, Joao W. Cangussu, Ray A. Decarlo, Aditya P. Mathur. An Overview of Software cybernetics [C]. In Proceedings of the Eleventh Annual International Workshop on Software Technology and Engineering Pratice, Washington: IEEE Computer Society Press, 2003: 77-86.
[19] Introduction to SDL 88. http://www.sdl.forum.org/sdl88tutorial/index. html, 2002.
[20] Marchand, H. and Samaan, M. Incremented design of a power transformer station controller using a controller synthesis methodology [J]. IEEE Transactions on Software Engineering, 2000, 26(8):729-741.
[21] X.Y. Wang, Y.C.Li and K.Y.Cai. On the polynomial dynamical system approach to software development [J]. Science in China (Series F), 2004, 47(4): 437-457.
[22] Baskar Sridharan, Aditya P. Mathur and Kai-Yuan Cai. Synthesizing distributed controller for safe operation of connected spaces [C]. In proceedings of the IEEE International Conference on Pervasive Computing and Communication, IEEE Computer Society Press, 2003: 452-459.
[23] Baskar Sridharan, Aditya P. Mathur and Kai-Yuan Cai. Using supervisory control to synthesize safety controllers for connectedspaces [C]. In Proceedings of the 3rd International Conference on Quality Software. IEEE Computer Society Press, 2003: 186-193.
[24] Joao, W. Cangussa, Raymond, A. D. and Aditya, P. M. Using sensitivity to validate a state variable model of the software test process [J]. IEEE Transactions on Software Engineering, 2003, 29(5): 430-443.
[25] Joao, W. Cangussu, Raymond, A. Decarlo and Aditya, P. M. A formal model of the software test process [J]. IEEE Transactions on Software Engineering, 2002, 28(8):782-796.
[26] Dellarocas, C., Klein, M. and Shrobe, H. An architecture for constructing self-evolving software systems [C]. In Proc. of the Third International Software Architecture Workshop, New York: ACM Press, 1998: 29-32.
[27] Bauer, A., Leucker, M. and Schallhart, C. Comparing LTL semantics for runtime verification [J]. Journal of Logic and Computation, 2010, 20(3):651-674.
[28] P. Oreizy et al. An architecture-based approach to self-adaptive software [J]. IEEE Intelligent Systems and their Application, 1999,14(2):54-62.
[29] Eisner, C., Fisman, D., Havlicek, J., Lustig, Y., McIsaac, A. Reasoning with temporal logic on truncated paths [C]. In Proceedings of the 15th International Conference on Computer Aided Verification (CAV’03), ACM Press, 2003: 27-39.
[30] Kamp, H. W. Tense Logic and the Theory of Linear Order [D]. Los Angeles: University of California, 1986.
[31] Andreas Bauer. Model-based runtime verification of distributed reactive systems[D]Munchen：TU Munchen，2007
[32]Bauer，A，Leucker，M and Schallhaxt，C Monitoring of reaRime properties[C] In Proceedings of Foundations of Software Technology and Theoretical Computer Science(FSTTCS’06)，Berlin：Springer-Verlag，2006：260-272
[33]Bauer，A，Leucker，M and Schallhart，C The good，the bad，and the ugly-ut how ugly is ugly?Technical Report TUM-10803[R]Munchen：TU Munchen，2008
[34]Martin Leucker and Christian Schallhaxt A brief account of mntime verification [Jll Journal of Logic and Algebraic Programming，2009，78(5)：293-303
[35]Bauer，A，Leucker，M and Schallhart，C The good，the bad，and the ugly-ut how ugly is ugly?[c]In Proceedings of the 7th International Workshop on Runtime Verification(RV’07)，Berlin：IEEE Society Press，2007：126-138
[36]Havelnnd，K Using runtime analysis to guide model checking ofjava programs [c]In Proceedings of the 7th International SPIN Workshop on SPIN Model Checking and Software Verification London，UK：Springer-Verlag，2000：245．264
[37]Havelund，K and Rosu，G Monitoring Java Programs with Java PathExplorer[Jll Electronic Notes in Theoretical Computer Science，2001，55(2)：97-1 14
[38]Havelund，K and Rosu，G Monitoring programs using rewriting[c]In ASE’01：Proceedings of the 16th IEEE International Conference on Automated Software Engineering Washington：IEEE Computer Society，2001：135-143
[39]Havelund，K and Rosu，G Synthesizing Monitors for Safety Properties[c]In Tools and Algorithms for Construction and Analysis of Systems，Springer Press，2002：342．356
[40]Havelund，K and Rosu，G Efficient Monitoring of Safety Properties Journal on Software Tools for Technology Transfer[Jll 2004，6(2)：1 58-173
[41]Clavel，M，Duran，F，Eker，S，Lincoln，P，Marti-Oliet，N Meseguer，J and Talcott，C The maude 2 0 system[C]In Proceedings of the 14th International Conference on Rewriting Techniques and Applications(RTA 2003)，Berlin：Springer-Verlag，2003：76-87
[42]Rosu，G and Bensalem，S Allen Linear(interval)temporal logic-translation to LTL and monitor synthesis[C]In International Conference on Computer Aided Verification(CAV)，Lecture Notes in Computer Science，2006，vol 4144：263-277
[43]Sen，K and Rosu，G Generating optimal monitors for extended regular expressions[Jll Electronic Notes in Theoretical Computer Science(ENTCS) 2003，89(2)：123-134
[44]Emersion，E A and Clarke，E M Characterizing correctness properties of parallel programs using fixpoints[c]In Proceedings of the 7th Colloquium onAutomata，Languages and Programming London：Springer-Verlag press，1980：169．181
[45]Kristoffersen，K J，Pedersen，C and Andersen，H R Runtime verification of timed LTL using disjunctive normalized equ~ion systems[J]Electronic Notes in Theoretical Computer Science，2003，89(2)2 10-225
[46]Bauer，A，Leucker，M and Schallhaact，C Model-based methods for the runtime analysis of reactive distributed systems[C]In Proceedings of the Australian Software Engineering Conference(ASWEC’06)IEEE Press，2006：243-252
[47]Chen，F and Rosu，G MOP：An Efficient and Generic Runtime Verification Framework[C]In Proceedings of the 22nd Annual ACM SIGPLAN Conference on Object-Oriented Programming，Systems，Languages and Applications (OOPSLA’07)，ACM Press，2007：569-588
[48]Chen，F and Rosu，G Towards monitoring-oriented programming：A paradigm combining specification and implementation[Jl Electronic Notes in Theoretical Computer Science(ENTCS)，2003，89(2)146-161
[49]Giannakopoulou，D and Havelund，K Runtime analysis of linear temporal logic specification[Rl，Tech Rep 01 21，RIACS／USRA 2001
[50]Stolz，V and Bodden，E Temporal assertions using AspectJ[Jll Electronic Notes in Theoretical Computer Science(ENTCS)，2006，144(4)：109-124[5 1]Finkbeiner，B and Sipma，H Checking finite traces using aRemaing automata[Jl Formal Methods in System Design，2003，24(2)：101-127
[52]D’A1Tlorim，M and Rosu，G Efficient monitoring of omega-languages[Jll In Intemational Conference on Computer Aided Verification(CAV)Lecture Notes in Computer Science，2007，vol 3576：364-378
[53]Dong W，Leucker M，SchalNart C Impartial anticipation in runtime verification [C]In Proc ofthe 6th Int’1 Symp on Automated Technology for Verification and Analysis(ATVA 2008)Heidelberg：Springer-Verlag，2008：386-396
[54]Sen，K and Rosu，G Generating optimal monRors for extended regular expressions [Jll Electronic Notes in Theoretical Computer Science (ENTCS)，2003，89(2)
[55]Martin，M C，Livshits，V B and Lam，M S Finding application errors and security flaw-s using PQL：a program query language[c]In Conference on Object-Oriented Programming，Systems，Languages，and Applications(OOPSLA)，New-York：ACM Press，2005：365-383
[56]Barringer，H，Goldberg，A，Havelund，K and Sen，K Program monitoring with LTL in Eagle[C]In Intemational Conference of Parallel and Distributed Processing Symposium(IPDPS)，New-Mexico：IEEE Society Press，2004
[57]Chris Allan，Pavel Avgustinov，Aske Simon Christensen，Laurie Hendren，Sasche Kuzins，Ondrej Lhotak,Oege de Moor，DaJnien Sereni，Ganesh Sittaanpalam，andJulian Tibble Adding trace matching with free variables to aspectJ In Proceedings of the 20th annual ACM SIGPLAN conference on Object-oriented programming，systems，languages，and applications，New-York：ACM Press，2005：345．364
[58]Pavel Avgustinov，Julian Tibble and Oege de Moor Making trace monitors feasible[Jll SIGPLAN，2007，42(10)：589-608
[59]Patrick Meredith，Dongyun Jin，Feng Chen and Grigore Rosu Efficient monitoring of parametric context-free patterns[Jll In Journal of Antomated Software Engineering，2010，17(2)：149-180
[60]Eric Bodden Efficient and Expressive Runtime Verification for Java[c]In Proceedings of the Grand finals of the ACM Student Research Competition，San Francisco：ACM Press，2005：123-134
[61]Barringer，H，Rydeheard，D E and Havelund，K Rule systems for run-time monitoring：From eagle to ruler[Jll Lecture Notes in Computer Science，2007，vol 4839：111．125
[62]D’Angelo，B，Sankaacanarayanan，S，Sanchez，C，Robinson，W，Finkbeiner，B，Sipma，H B，Mehrotra,S and Manna，Z LOLA：Runtime monitoring of synchronous systems [C] In International Symposium on Temporal Representation and Reasoning(TIME)ACM Press，2005：166-174
[63]Kim，M，Viswanathan，M，Kannan，S，Lee，I and Sokolsky，O Java-mac：A runtime assurance approach for java programs[Jll Formal Methods in System Design(FMSD)，2004，24(2)：129-1 55
[64]Kim，M，Kannan，S，Lee，I，Sokolsky，O and Viswanathan，M Computational analysis of run-time monitoring fundamentals ofjava-mac[Jll Electronic Notes in Theoretical Computer Science(ENTCS)，2004，70(4)：136-145
[65]Moonjoo，Kim Insup Lee，Usa Sammapun，Jangwoo Shin，Oleg Sokolsky Monitoring，Checking，and steering of Real-time Systems[c]In Proceedings of 2nd International Workshop on Runtime Verification，ENTCS，2002
[66]Moonjoo，Kim Insup Lee，Steering of Real-time Systems Based on Monitoring and Checking[C]In Proceedings of the Fifth International Workshop on Object-Oriented Real-time Dependable Systems，Washington：IEEE Computer Society,1999：1 1-21
[67]Oleg Sokolsky,Usa Sammapun，Insup Lee，Jesung Kim Run-time checking of Dynamic Properties[c]In Proceedings of Electr Notes Theor Comput Sci，IEEE Society Press，2006：91-108
[68]Rabin,M O and Scott，D Finite automata and thek decision problems[J]IBM Journal ofResearch and Development，1959，3：115-125
[69]Meyer，A R and Fischer，M J Economy of description by automata grammars，and formal systems[C]In Proc 12th IEEE Symp On Switching and AutomataTheory,IEEE Society Press，1971：188-191
[70]Sistla，A P and Clarke，E M Complexity of propositional temporal logics[Jll Journal ofthe ACM(JACM)，1985，32(3)：733-749
[71]B~chi，J R On a decision method in restricted second order arithmetic[c]In Proc Intemational Conference on Logic，Method and Philosophe，Stanford：Stanford University Press，1962：1-12
[72]Sistla，A P，Vaacdi,M Y and Wolper，P The complementation problem for B~chi automata with applications to temporal logic[Jll Theoretical Computer Science，1987，49：217-237
[73]Safra，S On the complexity of omega-automata[C]In Proceedings of the 29th Annual Symposium on Foundations of Computer Science，FoCS’88，Los Alamitos：IEEE Computer Society Press，1988：3 19-327
[74]Alpern，B and Schneider，F B[c]Recognizing safety and liveness Distributed Computing，1987，2(3)：1 17-126
[75]Brzozowski，J A and Leiss，E Finite automata and sequential networks[Jll Theoretical Computer Science，1980，10：19-35
[76]Chandra，A K，Kozen，D C and Stockmeyer，L J Alternation[Jll Journal of the Association for Computing Machinery,1981，28(1)：1 14-133
[77]Emst Leiss Succinct representation ofregular languages by Boolean automata[c] Theorectical Computer Science，1981，38(13)：323-330
[78]Muller，D E and Schupp，P E Alternating automata on infinite trees[Jll Theoretical Computer Science，1987，54：267-276
[79]Miyano，S and Hayashi，T Alternating finite automata on f11-words[Jll Theoretical Computer Science，1984，32：321-330
[80]Pnueli，A The temporal logic of programs[c]In Proceedings of the 1 8th IEEE Symposium on the Foundations of Computer Science(FOCS’77)Providence：IEEE Computer Society Press，1977：125-137
[81]Thomas，W Automata on infinite objects[Jll In Handbook of Theoretical Computer Science，vol B，chap 4 Elsevier Science Publishers B V，133-191
[82]Lamport，L What good is temporal logic?[c]In Proceedings of the IFIP 9th World Computer Congress，IEEE Society Press，1983：657-668
[83]Pnueli，A Application of temporal logic to the specification and verification of reactive systems：a survey of current trends[c]In Current trends in concurrency Overviews and tutorials，New-York：Springer-Verlag，1986：510-584
[84]Dwyer，M B，Avrunin，G S and Corbett，J C Patterns in Prope~y Specification for nnite-state verification[C]In Intemational Conference on Software Engineering(IcsE)New-York：ACM Press，1999：41 1-420
[85]Baresi，L，Guinea，S and Pasquale，L Towards a unified framework for themonitoring and recovery of bpel processes．In Proceedings of TAV-WEB．New- York：ACM，2008：15-19
[86]Muller，D E Saoudi，A and Schupp，P E Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential time[c]In Proceedings of 3rd IEEE Symposium on Logic in Computer Science，Edinburgh：IEEE Press，1988：422-427
[87]Barbon，F，Traverso，P，Pistore，M and Trainotti，M Run-time monitoring of instances and classes of web service compositions[c] In International Conference on Web Services(ICWS)Washington：IEEE Computer Society, 2006：63．71
[88]Vaxdi，M Y Nontraditional applications of automata theory[Jll Lecture Notes in Computer Science，1994，volume 789：575-597
[89]Vardi，M Y and Wolper，P Reasoning about infinite computations[Jll Information and Computation，1994，1 15(1)：1-37
[90]Kupferman,O and Vardi，M Y Model Checking of Safety Properties[Jl Formal Methods in System Design(FMSD)，2001，19(3)：291-314
[91]Geilen，M On the Construction of monitors for temporal logic properties[Jll In Electronic Notes in Theoretical Computer Science，2001，55(2)：181-199
[92]Bauer A，Leucher M，Schallhaxt C Runtime verification for LTL and PTLTL[R] Technical Report，TUM-10724，Mfinchen：TU Mfinchen，2007
[93]Vaxdi，M Y，Wolper，P An automata-theoretic approach to automatic program verification[c]In Proceedings of Logic in Computer Science(LICS)，1986：332．345
[94]Corber,J Dwyer，M，Hatclifl．J，Pasareamu，C，Laubach，S and Zheng，H Bandera：Extracting fmite-state models from java source code[c]In proceedings of the 22nd International Conference on Software Engineering(IcsE)，2000：439．448
[95]Havelund，K and Pressburger，T Model checking java programs using Java PathFinder[Jll International Journal on Software Tools for Technology Transfer，2000，2(4)：366-381
[96]Feather，M S，Fickas，S，Van Lamsweerde，A and Pondard，C Reconciling system requirements and runtime behavior[C]In 9th International Workshop on Software Specification and Design，New-York：IEEE Computer Society，1998：50．59
[97]Arvind Easwaran，Sampath Kannan，and Oleg Sokolsky Steering of discrete event systems：control theory approach[Jll In Electronic Notes in Theoretical Computer Science，2005，144(4)：21-39
[98]Schwoon，S and Espaxza，J A note on on-the-fly verification algorithms[Jl In tools and Algorithms for the construction and analysis of Systems(TACAS)Lecture Notes in Computer Science，2006 vol 3440：174。190
[99]Feng chen，Choonghwan Lee，Grigore rosu Mining parametric specifications[R] Illinois：University of Illinois，20 10
[100]Choonghwan Lee，Feng Chen，Grigore Rosu Mining parametric specifications [C]In Proceedings ofthe 30th International Conference on Software Engineering，2011
[101]Hao Chen，David Wagner MOPS：an Infrastructure for Examining Secur~y Properties of Software In Proceedings of ACM Conference on Computer and Communications Secur~y，Chicago：ACM Press，1993：109-121
[102]Patrick O’Neil Meredith，Dongyun Jin，Dennis Griffith，Feng Chen，Grigore Rosu An overview ofthe mop runtime verification framework[c]，Springer，20 1 1
[103]Sheng-Luen Chung，Stephane Lafortune，and Feng Lin Limited lookaJaead policies in supervisory control of discrete event systems[Jll In IEEE Transactions on Automatic Control，1992，Volume 37：(18-31)
[104]Sheng-Luen Chung，Stephane Lafortune，and Feng Lin Supervisory control using variable lookahead policies[c]In Proceedings of Discrete Event Systems Kluw-er．1994
[105]Kim，M，Viswanathan，M，S K Haaaene Ben-Abdallah，Lee，I and Sokolsky，O Formally specified monitoring of temporal properties[c]In proceedings of European Conference on Real-time Systems，1999
[106]Stolz，V Temporal assertions with paacameterized propositions[Jll Journal of Logic and Computation，2008
[107]Stolz，V Temporal assertions for sequential and concurrent programs[D]，Aachen：RWTH University，2007：176-187
[108]Stolz V and Bodden，E Temporal Assertions using AspectJ[c]In Proceedings offifth workshop on Runtime verification(RV’05)，2005：201-216
[109]Stolz，V and Huch，F Runtime Verification of Concurrent Haskell Programs[J] Electronic Notes in Theoretical Computer Science(ENTCS)，2005，1 13：201-216
[110]Va*di MY An automata-theoretic approach to linear temporal logic[C]In Proc of the Logics for Concurrency：Structure Versus Automata,New-York：Springer-Verlag，1996：238266
[111]Java Technology Center，Compaq Corp Compaq JTrek Online documentation：http：／／www digital com／java／download／jtrek／2008
[112]Bauer，A，Leucker，M and Schallhart，C Runtime verification for LTL andTuL[Jll ACM Transactions on Software Engineering and Methodology(TOSEM)，20 10 In press
[113]Feng Chen and Grigore Rosu Parametric trace slicing and monitoring In TACAS，volume 5505 of Lecture Notes in Computer Science，Springer Press，2009：246-261
[114]Grigore Rosu and Feng Chen Parametric Trace Slicing and Monitoring[Rl，Technical Report，UIUCDCS-R-2008-2977，Illinois：University of Illinois，2008
[115]Memcheck,http：／／valgrind org 2007
[116]Loscocco，P A，Smalley，s D，Muckelbauer，P A，Taylor，R C，Turner，s J and Farrell，J F The inevitability offailure：The flawed assumption of security in modern computing environments[c]In Proceedings of the 21st National Information Systems Security Conference，New-York：IEEE Society Press，1998：303．314
[117]Abrams，M D，Jajodia,S，Podell，H J Information Security：An Integrated Collection ofEssays[Rl，IEEE Comp 1995
[118]Lepreau，J The Persistent Relevance of the Local Operating System to Global Applications[c]In Proceedings of the 7th ACM SIGOPS European Workshop，1996
[119]Andrei SabeHbld and Andrew-C Myers Language-based information-flow- security[Jl IEEE Journal on Selected Areas in Communication，2003，21(1)：5-19
[120]Herzog，A and Guttman，J Achieving security goals with Security-Enhanced Linux[Rl，Tech rep，Mitre Corporation，2002
[121]Joshua D Guttman，Amy L Herzog，John D Ramsdell，Clement W Skorupka Verifying information flow-goals in Security-Enhanced Linux[Jll Journal of Computer Security，2005，13(1)：115-134
[122]Changzhi Zhao，Wei Dong，Zhichang Qi Active Monitoring for Control Systems under Anticipatory Semantics[c] In proceedings of 10th International Conference on Quality Software，Zhangjiajie：IEEE CPS，2010：318-325
[123]Chaaagzhi Zhao，Wei Dong，Ji Wang，Ping Sui and Zhichang Qi Software Active Online Monitoring Under Anticipatory Semantics[C]In Proceedings of 1st International Workshop on Software Health Management Online Published at http：／／www isis vanderbiR-edu／workshops／smc-it-2009-shm／，2009
[124]Randal E Bryant Graph-Based Algorithms for Boolean Function Maniputation l Jl Journal ofIEEE Transactions on Computers，1986，35：677-691
[125]A W Roscoe alad M H Goldsmith What is intransitive noninterference?[c]In Proceedings of 12th IEEE Computer Security Foundation Workshop 2003
[126]SLAT：SELinux policy file analysis tool http：／／www dsi unive it／- IFIPWGl 7Vits2003 html 2004