User Guide: Decentralized Runtime Verification of LTL Specifications in Distributed Systems Tool (ICI-363)

User Guide: Decentralized Runtime Verification of LTL Specifications in Distributed Systems Tool (ICI-363)
Minimum Subscription Required:
Designer
Price for Canadian Academics
$0.00

How to access this item?

Contact Us

Need help? Any feedback?

Please email us at: docs@cmc.ca.

Description

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 licensing@cmc.ca or 613-530-4787.


Acknowledging CMC

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 Acknowledge CMC.