14
views
0
recommends
+1 Recommend
0 collections
    0
    shares
      • Record: found
      • Abstract: found
      • Article: found
      Is Open Access

      Concurrency-Preserving and Sound Monitoring of Multi-Threaded Component-Based Systems

      Preprint
      , , ,

      Read this article at

      Bookmark
          There is no author summary for this article yet. Authors can add summaries to their articles on ScienceOpen to make them more accessible to a non-specialist audience.

          Abstract

          This paper addresses the monitoring of logic-independent linear-time user-provided properties in multi-threaded component-based systems. We consider intrinsically independent components that can be executed concurrently with a centralized coordination for multiparty interactions. In this context, the prob- lem that arises is that a global state of the system is not available to the monitor. A naive solution to this problem would be to plug in a monitor which would force the system to synchronize in order to obtain the sequence of global states at runtime. Such a solution would defeat the whole purpose of having concurrent components. Instead, we reconstruct on-the-fly the global states by accumulating the partial states traversed by the system at runtime. We define transformations of components that preserve their semantics and concurrency and, at the same time, allow to monitor global-state properties. Moreover, we present RVMT-BIP, a prototype tool implementing the transformations for monitoring multi-threaded systems described in the BIP (Behavior, Interaction, Priority) framework, an expressive framework for the formal construction of heterogeneous systems. Our experiments on several multi-threaded BIP systems show that RVMT-BIP induces a cheap runtime overhead.

          Related collections

          Most cited references22

          • Record: found
          • Abstract: not found
          • Article: not found

          Comparing LTL Semantics for Runtime Verification

            Bookmark
            • Record: found
            • Abstract: not found
            • Article: not found

            What can you verify and enforce at runtime?

              Bookmark
              • Record: found
              • Abstract: not found
              • Book Chapter: not found

              Communicating Sequential Processes

              C. Hoare (2002)
                Bookmark

                Author and article information

                Journal
                2016-12-19
                Article
                1612.06154
                4260de97-5f3b-404c-ae9f-db7058b8e670

                http://arxiv.org/licenses/nonexclusive-distrib/1.0/

                History
                Custom metadata
                cs.SE

                Software engineering
                Software engineering

                Comments

                Comment on this article