JavaMOP 1.0 Past Time Linear Temporal Logic with Calls and Returns (JavaPTCaRet) Plugin

Jump to: navigation, search

This version of JavaMOP is old and not supported anymore! Go to the JavaMOP webpage for the latest version.



This is JavaMOP1.0, which is now deprecated. Go to JavaMOP for the current version.

  

MOP

ERE

CFG

PTLTL

FTLTL

PTCaRet

...

JavaMOP

JavaERE

JavaCFG

JavaPTLTL

JavaFTLTL

JavaPTCaRet

...

BusMOP

BusERE

...

BusPTLTL

... ... ...
... ... ... ... ... ... ...
MOP Matrix: a clickable map of MOP pages.


Contents

Overview

ptCaRet extends the past time linear temporal logic (PTLTL) with call/return atoms. In addition to the standard temporal operators, it also includes abstract variants of past temporal operators, which can express properties over traces in which terminated function or procedure executions are abstracted away into a call and a corresponding return. This way, ptCaRet can express safety properties about procedural programs which cannot be expressed using conventional linear temporal logics.

Input

PTCaRet formulae use the following syntax, which is defined in BNF (extended with the common {p} for zero or more and [p] for zero or one repetitions of p, respectively):

<Formula> ::= "true" | "false" | <Event Name> | <Formula> "and" <Formula> | <Formula> "or" <Formula> 
| "not" <Formula> | <Formula> "implies" <Formula> <!-- Normal boolean constants and operators>
| "(*)" <Formula> | <Formula> "S" <Formula> | "<*>" <Formula> | "[*]" <Formula> <!-- Standard temporal operators>
| "(*a)" <Formula> | <Formula> "Sa" <Formula> | "<*a>" <Formula> | "[*a]" <Formula> <!-- abstract temporal operators>
| "@b" <Formula> | "@c" <Formula> <!-- derived temporal operators: at begin and at call>
| <Formula> "Ss@b" <Formula> | "<*s@b>" <Formula> | "[*s@b]" <Formula> <!-- derived begin stack operators>
| <Formula> "Ss@c" <Formula> | "<*s@c>" <Formula> | "[*s@c]" <Formula> <!-- derived call stack operators>
| <Formula> "Ss@bc" <Formula> | "<*s@bc>" <Formula> | "[*s@bc]" <Formula> <!-- derived begin-or-call stack operators>

Unary operators have higher precedence than binary operators. The binary operators in decreasing order of precedence are and > or > implies > S*; here S* includes all the variants of the since operator. Please refer to the corresponding technical report for formal definitions of these operators.

Output

Intermediate Java code used by JavaMOP for the PTCaRet formula specified.

Run the JavaPTCaRetPlugin Online

  • Note: The name of the generated Aspect will be the name of the first specification in the text box + MonitorAspect. The name of the .aj file you intend to compile needs to be the same. For example, for LeakingSyncCFG, the generated aspect is LeakingSyncCFGMonitorAspect, and should be placed in a file named LeakingSncCFGMonitorAspect.aj.
  • Note: One may append within or !within clauses to the event definitions in JavaMOP to control the scope of instrumentation. For example, if it is certain that some class C will not trigger any event of interest, one may use !within(C) in the event definitions to ignore C during the instrumentation, improving the instrumentation efficiency. The syntax of the within clause can be found in the AspectJ documentation.
Choose an example:
  • SafeFile
  • SafeLock
 

Please press the Run button once and wait; it may take a few seconds to run JavaMOP1.0_PTCARET; the execution of JavaMOP1.0_PTCARET using this web interface is limited to 2 minutes of CPU time and 500 MB of RAM.

Personal tools
Namespaces

Variants
Views
Actions
Navigation