The LySa Toolkit in Eclipse(LyTE) was designed to help developers work with the LySa code generated by Elyjah. It aims to make LySa slightly less intimidating to any developers who were introduced to the process calculus through Elyjah. Like Elyjah it is also implemented as an Eclipse plugin so much of the operation will be familiar to developers who should not have to learn how to use a new tool in order to learn a new language. A screenshot of LyTE running in Eclipse is presented below.

LySa Editor

The LySa Editor is designed to help developers write and edit LySa models. It features dynamic parse checking to identify errors speedily and provide the developers with a useful error message and suggested fixes. Fitting in to the Eclipse platform, the error is underlined, the line marked, and an error message added to the problem console. This checking can identify syntax flaws such as using the wrong punctuation, misspelt key words or missing pattern matching on receive and decrypt messages. The editor also provides syntax highlighting, which helps separate send, receive and decrypt processes by highlighting them in different colours. There is additional static analysis which checks that for each send process there is a corresponding possible receive process with the same source and destination as well as the right number of tuples. This provides a weak form of liveness checking that warns users of possible areas of deadlock in their models. The user's LySa model can then be analysed with the LySatool, the results of which are displayed in an Eclipse console.

AnaLySa

This tool translates a LySa model into standard protocol narration. Standard protocol narrations are often used to describe protocols, although the trouble is that they only contain half of the protocol. Namely they do not say what the recipient does upon receiving a message. However, they are used because they succinctly describe the messages exchanged. A protocol narration is generated from a LySa process by creating a table of LySa send processes and the receive process that comes before each one. This enables the order of send processes to be worked out, starting by looking for the send process with no previous receive command. After the first message is identified, the matching receive process for this message is found and using the previously-generated table the next send process can be discovered. This process continues for all send processes.

VisuaLySa

An alternative to the protocol narration is a visual representation of the protocol. This option is provided by the VisuaLySa which translates a LySa process into a sequence-diagram style diagram. This sort of option is useful for developers who are playing around with LySa and trying to learn how it works through experimentation. An example of VisuaLysa is shown in the generated visual representation of the Otway-Rees protocol below.

A different graphical representation of a protocol is provided as well as the sequence diagram. This is an animation of the messages sent between various principals which can be run as an animation or by stepping through in a single step manner. This is seen in below. After the protocol is terminated the diagram shows the flow of communication that occurred during the protocol run.

Sample Videos