Hosein Nazarpour, Yliès Falcone, Saddek Bensalem, Marius Bozga
RVMT-BIP: A Tool for the Runtime Verification of Multi-Threaded Component-Based Systems (2016)
RVMT-BIP: A Tool for the Runtime Verification of Multi-Threaded Component-Based Systems (2016)
TR-2016-2.pdf
Keywords: component-based design, multiparty interaction, multi-threaded, monitoring, concurrency, runtime verification
Abstract: RVMT-BIP is a tool for the runtime verification of multi-threaded component-based systems described in the Behavior, Interaction, Priority (BIP) framework against linear-time and logic-independent properties.RVMT-BIP implements rigorous semantics-preserving transformations of BIP systems to instrument and inject a sound and concurrency-preserving global-state reconstructor for on-the-fly monitoring. Our experiments on several multi-threaded BIP systems show that RVMT-BIP generally induces a cheap runtime overhead, especially when the system is highly concurrent.
