DIANA (DIstributed ANAlysis tool)

DIANA is a tool to efficiently monitor safety properties in distributed systems. It uses a variant of past-time linear temporal logic called PT-DTL (past time distributed temporal logic) that allows a process to assert a temporal formula involving its local state and "remote expressions" and "remote formulae". Remote expressions are expressions evaluated at other processes at the last state the current process is aware of. This makes this logic fairly intuitive and easy to use. See the examples sections for some properties of well-known distributed algorithms.

For more details about the logic, the framework and the monitoring algorithm please refer to the following paper:

[ps] [pdf] “Efficient Decentralized Monitoring of Safety in Distributed Systems ” Koushik Sen, Abhay Vardhan, Gul Agha, and Grigore Rosu

The tool and the framework can be downloaded here

Here are some examples of properties that can be expressed in PT-DTL:

• The first example regards the well known problem of leader election for a network of processes. The key requirement for leader election is that there is at-most one leader. If there are n processes and state is a variable in each process that can have values {leader, loser, candidate, sleep,} then we can write the property at every process as: ``if a leader is elected then if the current process is a leader then, at its knowledge, none of the other processes is a leader''. We can formalize this requirement as the following PT-DTL formula:
  
  
  Here, "@" should be read as "at" and @E and should be thought of as the value of E in the most recent local state of the remote process that the current process is aware of.
  
  Given an implementation of the leader election problem, one can monitor this formula at every process. If violated, then clearly the leader election implementation is wrong.
  

• The second example is concerned with a number of processes which vote on a particular resolution. The desired property, ``if the resolution is accepted then more than half of the processes say yes'', can be stated as:


Here, a process stores 1 in a local variable vote if it is in favor of the resolution, and 0 otherwise.

• The third example is a safety property that a server must satisfy in case it reboots itself. The property is that ``server accepts to reboot only after knowing that each client is inactive and aware of the warning to reboot''. The property can be written as a server-local formula as follows: