Bus Past Time Linear Temporal Logic (BusPTLTL) Plugin
From FSL
 |
|
 |
|||||
|---|---|---|---|---|---|---|---|
| ... | |||||||
| ... | |||||||
| ... |
BusPTLTL |
... | ... | ... | |||
| ... | ... | ... | ... | ... | ... | ... | ... |
| MOP Matrix: a clickable map of MOP pages. | |||||||
BusPTLTL is an instance of MOP for monitoring PCI Bus traffic and for PTLTL specifications. This instance is technically unnecessary, since one can simply run BusMOP with PTLTL specifications, which is precisely what the online interface below does. BusPTLTL has, however, conceptual (and potentially theoretical) value; many Bus users prefer to specify properties exclusively as parametric regular patterns. Enter your PTLTL specification in the form below or chose (and modify) one example from the menu - provided examples are also reachable from the menu of the main BusMOP interface. Go to BusMOP for instructions on how download and install it, as well as on how to compile the AspectJ monitors generated below.
Note: if there are any technical difficulties please alert pmeredit@cs.uiuc.edu
Please press the Run button once and wait; it may take a few seconds to run BusMOPptLTL; the execution of BusMOPptLTL using this web interface is limited to 2 minutes of CPU time and 500 MB of RAM.
