{"id":930,"date":"2020-11-25T04:20:53","date_gmt":"2020-11-25T04:20:53","guid":{"rendered":"http:\/\/se.kaist.ac.kr\/starlab\/?page_id=930"},"modified":"2020-11-25T04:20:53","modified_gmt":"2020-11-25T04:20:53","slug":"runtime-monitoring-verification-technique","status":"publish","type":"page","link":"https:\/\/se.kaist.ac.kr\/starlab\/studies\/study-2-statistical-verification-of-sos\/runtime-monitoring-verification-technique\/","title":{"rendered":"Runtime Monitoring & Verification Technique"},"content":{"rendered":"

Runtime Monitoring<\/h4>\n

In general, runtime monitoring has 2 main approaches, online and offline monitoring. In online monitoring, a system is monitored during its runtime for execution for any violation(s) of specified properties. A runtime monitor will continuously receive information in terms of system events which are generated by the monitored system. Based on the events received so far, the runtime monitor has to determine if any violations have occurred up till that point in time.<\/p>\n

Due to its capability to monitor a system as it executes, online monitoring also provides the ability to make early detections which are crucial for properties which may require immediate action upon violation. These properties include safety and critical properties. On the other hand, this capability also introduces a runtime overhead on the system. A spectrum of runtime monitoring online approaches will be discussed later in this report.<\/p>\n

In offline monitoring, a monitor takes as input a complete execution trace from a system which has already finished executing and analyses the complete trace for any possible violation of specified properties. This means that no monitoring is performed during a system\u2019s execution phase.<\/p>\n

Offline monitoring, while not as intrusive as online monitoring, suffers from late detection as it is not able to monitor a system\u2019s execution trace during a system\u2019s runtime execution and is only able to perform analysis once the systems finishes its execution and generates a complete execution trace for the monitor. The table below shows a comparison between offline and online monitoring.<\/p>\n\n\n\n\n\n\n\n\n\n
 <\/td>\nOffline Monitoring<\/td>\nOnline Monitoring<\/td>\n<\/tr>\n
Monitoring execution<\/td>\nAfter monitored system terminates (trace is forwarded to offline monitor)<\/td>\nWhile executing the system<\/td>\n<\/tr>\n
Relation with system<\/td>\nIndependent from the system<\/td>\nExecute alongside the system<\/td>\n<\/tr>\n
Monitoring overhead<\/td>\nLittle runtime overhead<\/td>\nInevitable runtime overhead<\/td>\n<\/tr>\n
Violation detection<\/td>\nLate detection (detection happens after system stops executing)<\/td>\nEarly detection<\/td>\n<\/tr>\n
Suitable verification property<\/td>\nProperties that can be verified by globally analyzing the execution trace<\/td>\nSecurity and critical properties<\/td>\n<\/tr>\n
Suitable to use<\/td>\nDouble checking the behavior of systems<\/td>\nPower plant controller<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n

 <\/p>\n

Online Runtime Monitoring Spectrum<\/h4>\n

Cassar et al. (2017) introduced a spectrum for the different online runtime monitoring approaches (in terms of component-based systems) as seen in the figure above. Briefly, component-based systems are made up of entities such as actors, nodes, threads, and etc that can be in a running<\/i> or blocked state.<\/p>\n

The spectrum includes Completely Synchronous (CS)<\/i> monitoring instrumentation, Synchronous Monitoring with Synchronous Instrumentation (SMSI)<\/i>, Asynchronous Monitoring with Checkpoints (AMC)<\/i>, Asynchronous Monitoring with Synchronous Detections (AMSD)<\/i> and Completely Asynchronous (CA)<\/i> monitoring approach.<\/p>\n

The spectrum is (as seen in the above figure) is ranked from left to right in order of tightly coupled systems to loosely coupled systems. A tightly coupled system blocks the system every time an event occurs thus allowing for more control over the system at the cost of introducing overhead. On the other end, a loosely coupled system does not perform any system blocking when an event occurs resulting in more efficiency in terms of lesser overhead at the cost of sacrificing the degree of control over the system.<\/p>\n

For SMSI, AMC,<\/i> and AMSD,<\/i> these approaches fall in between the extreme ends of the spectrum which shows the compromise between the overhead and degree of control over the system as a whole.<\/p>\n

    \n
  • CS <\/i>monitoring<\/li>\n<\/ul>\n

    On the left end of the spectrum, the CS<\/i> monitoring instrumentation approach refers to the tight coupling between the runtime monitor and the system. When an event occurs in any one particular component of the system, all system components are blocked and remain blocked until the required monitoring checks are performed after which the system components are then unblocked.<\/p>\n

    This approach allows the runtime property to be immediately detected as all system components are blocked when a violation of the said property detected. Conversely, this tightly coupled behavior is a highly intrusive approach due to the required amount of synchronization between the system, system events and the monitor which results in introducing higher performance overhead on the monitored system.<\/p>\n

      \n
    • SMSI<\/i><\/li>\n<\/ul>\n

      The SMSI<\/i> approach also falls close to the left of the spectrum suggesting that it is a tightly coupled approach but with some caveats. Similar to the CS<\/i> approach, whenever a specified event is executed, blocking occurs. The difference is that instead of blocking the entire system, only the component responsible for the execution of the event is blocked. The components remains blocked until the necessary monitoring steps are completed and are then reset to its running state.<\/p>\n

      Other components in the system which are not responsible for causing the (monitored) event to occur are allowed to continue executing. However, as all events generated by the system still has to be inspected by the monitor synchronously, it causes this approach to still be highly intrusive (albeit not as intrusive as the CS <\/i>approach) which in turn introduces performance overhead.<\/p>\n

        \n
      • AMC<\/i><\/li>\n<\/ul>\n

        AMC<\/i> provides a balanced approach of allowing the user to specify the components and its generated events which require synchronization with the runtime monitor. A specified component which requires synchronization with the monitor has to temporarily block its execution and await for synchronization while non-specified components may continue with its execution uninterrupted.<\/p>\n

        This approach allows uses to manually determine the level of control and intrusiveness the monitor has over the system such as specifying checkpoints for critical events, whereby the system has to block its execution and remain blocked until the runtime monitor has completed the necessary checks. This also means that other general non critical events do not cause the system to be blocked.<\/p>\n

          \n
        • AMSD<\/i><\/li>\n<\/ul>\n

          The AMSD<\/i> approach lies closer to the right side of the spectrum which means that the runtime monitor and the system is much more loosely coupled than the previous approaches. In particular, this approach only performs synchronization between system events which may cause a violation and the runtime monitor.<\/p>\n

          For example, if a particular component generates a specified event which may cause a violation, only that component is blocked and other components which do not contribute to the event may continue its execution. Therefore, this approach still allows for runtime detections (for specified system events) while minimizing its intrusiveness to the system.<\/p>\n

            \n
          • CA Monitoring<\/i><\/li>\n<\/ul>\n

            On the far right end of the spectrum, the CA monitoring<\/i> approach is completely asynchronous and loosely coupled. This means that the runtime monitor does not perform any form of blocking for all events generated by the system and its components. The handling and checking of events are performed independently by the runtime monitor from the system.<\/p>\n

            Oftentimes, this approach may be mistaken for a form of offline monitoring due to its loosely coupled and asynchronous characteristics, similar to the offline monitoring approach. The caveat is that offline monitoring requires complete execution traces which are only obtainable once a system finish its execution whereas CA monitoring <\/i>analyses partial incremental traces during the runtime of a system.<\/p>\n

            CA monitoring<\/i>, although extremely non-intrusive, suffers from late detection. Even if violation causing events were to be detected by the monitor, as no form of component blocking is carried out, the violation would not be flagged in time for any sort of mitigating response to be carried out.<\/p>\n

             <\/p>\n

            Runtime Monitoring Approaches implemented in tool<\/h4>\n

            Based on the above discussed approaches, the below table shows a categorization of existing tools and the approach type it belongs to.<\/p>\n\n\n\n\n\n\n\n\n
            Tool<\/td>\nOnline<\/td>\nOffline<\/td>\n<\/tr>\n
            CS<\/td>\nSMSI<\/td>\nAMC<\/td>\nAMSD<\/td>\nCA<\/td>\n<\/tr>\n
            JEAGLE<\/td>\n <\/td>\n\u25cf<\/td>\n <\/td>\n <\/td>\n <\/td>\n <\/td>\n<\/tr>\n
            Java-MOP<\/td>\n <\/td>\n\u25cf<\/td>\n <\/td>\n <\/td>\n\u25cf<\/td>\n\u25cf<\/td>\n<\/tr>\n
            LARVA toolkit<\/td>\n <\/td>\n\u25cf<\/td>\n <\/td>\n <\/td>\n\u25cf<\/td>\n\u25cf<\/td>\n<\/tr>\n
            detectEr toolkit<\/td>\n <\/td>\n\u25cf<\/td>\n\u25cf<\/td>\n\u25cf<\/td>\n\u25cf<\/td>\n <\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n

            JEAGLE is a Java implementation of Eagle, which is a runtime verification tool supporting future and past time logics, interval logics, state machines, extended regular expression and real-time and ata constraints. JEAGLE implements SMSI by converting specified runtime monitoring properties in Java code and uses AOP to inline the necessary monitoring code into the monitored application. Inlining is the method of replacing functions call with the actual body of the function itself.<\/p>\n

            Java-MOP is a client-server Java tool for runtime monitoring and verification using the monitoring oriented programming (MOP) concept. MOP is a paradigm which combines specification and implementation to form a system. During runtime, the specification is checked against the execution trace created by the implementation. Interaction between specification and implementation occurs in the form of an example of providing recovery code for execution during violation of a safety specification. (ref: Chen, Feng & Ro\u015fu, Grigore. (2003). Towards Monitoring-Oriented Programming. Electronic Notes in Theoretical Computer Science – ENTCS. 89. 108-127. 10.1016\/S1571-0661(04)81045-4. )<\/i><\/p>\n

            Java-MOP supports specification languages such as past and future-time LTL, extended regular expressions and other. It supports offline monitoring, CA approach and SMSI approach by inlining verification checks. Automated code instrumentation is done by Java-MOP to inline the monitoring verification code within the application.<\/p>\n

            LARVA-toolkit is a Java runtime verification tool for object oriented systems. Using an automata-based specification language called Dynamic Automata with Timers and Events (DATE), it allows users to specify real-time and discrete-time properties in terms of automata. The DATE specification is converted into an offline monitor or an online monitor; an online monitor using the SMSI approach. Verification checks are inserted into the monitored application and its specified components using AOP instrumentation.<\/p>\n

            The detecEr toolkit is a framework for runtime monitoring in Erlang systems. It converts properties specified in Hennessey Milner logic with recursion into monitors. Its capabilities include allowing for CA, SMSI, AMC and AMSD approaches. Code instrumentation is achieved using an AOP framework for Erlang called eAOP. Th eAOP framework reports events to the runtime monitor as asynchronous messages and is able to force some system components to block while waiting for feedback from monitor thus giving it synchronous capability.<\/p>\n

            RV-Monitor is a re-implementation of Java-MOP by separating its monitoring from its code instrumentation capabilities and improved its efficiency in terms of monitoring multiple properties at the same time and the merging of index trees used in the original Java-MOP\u2019s indexing algorithm. Other improvements include removing the behavior for multiple weak references to a single object caused by monitoring a single specification by using a global weak reference table (GWRT) that uses only one weak reference for each distinct object.<\/p>\n

            ReMINDS is a runtime monitoring framework designed for monitoring System of Systems (SoS) and its constituent systems. It uses an event model for analyzing and managing events that occur at runtime. Generated events are sent to the ReMINDS framework during runtime, which is made possible by probes instrumenting the monitored system. At its core, ReMINDS is made up of four layers responsible for specific parts in the entire monitoring process, and another layer which cross cuts into each layers for managing variability.<\/p>\n","protected":false},"excerpt":{"rendered":"

            Runtime Monitoring In general, runtime monitoring has 2 main approaches, online and offline monitoring. In online monitoring, a system is monitored during its runtime for execution for any violation(s) of specified properties. A runtime monitor will continuously receive information in terms of system events which are generated by the monitored system. Based on the events […]<\/p>\n","protected":false},"author":1,"featured_media":0,"parent":340,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":[],"_links":{"self":[{"href":"https:\/\/se.kaist.ac.kr\/starlab\/wp-json\/wp\/v2\/pages\/930"}],"collection":[{"href":"https:\/\/se.kaist.ac.kr\/starlab\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/se.kaist.ac.kr\/starlab\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/se.kaist.ac.kr\/starlab\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/se.kaist.ac.kr\/starlab\/wp-json\/wp\/v2\/comments?post=930"}],"version-history":[{"count":1,"href":"https:\/\/se.kaist.ac.kr\/starlab\/wp-json\/wp\/v2\/pages\/930\/revisions"}],"predecessor-version":[{"id":931,"href":"https:\/\/se.kaist.ac.kr\/starlab\/wp-json\/wp\/v2\/pages\/930\/revisions\/931"}],"up":[{"embeddable":true,"href":"https:\/\/se.kaist.ac.kr\/starlab\/wp-json\/wp\/v2\/pages\/340"}],"wp:attachment":[{"href":"https:\/\/se.kaist.ac.kr\/starlab\/wp-json\/wp\/v2\/media?parent=930"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}