User Guide: Decentralized Runtime Verification of LTL Specifications in Distributed Systems Tool (ICI-363)
Minimum Subscription Required:
Price for Canadian Academics
Prepared by Menna Hasabelnaby and Dr. Borzoo Bonakdarpour, Department of Computing and Software, McMaster University; in co-operation with CMC Microsystems.
This document describes how to run the MCDemo tool and check the results. It can be studied to understand runtime monitoring of software.
MCDemo is a runtime monitoring tool that runs on a distributed system of n devices. Each device runs a simple program that loads a trace file containing events such as variable changes and device communications. The monitor reads the trace events and notifies the program if the global state of the program reaches a final state in the linear temporal logic (LTL) property automaton.
Licensing Requirements or Restrictions
All CMC account holders with a Professor Research Subscription are authorized to access this document. For more information, contact firstname.lastname@example.org or 613-530-4787.
If your research benefits from products and services provided by CMC Microsystems, please acknowledge this support in any
publications about your work. For more information, please visit