TwoTowers 5.1

TOOL DESCRIPTION

Most of the research activity of Marco Bernardo has resulted in the development of TwoTowers, an open-source software tool for the functional verification, security analysis, and performance evaluation of computer, communication and software systems modeled in the architectural description language Æmilia, which is based on the stochastic process algebra EMPAgr.

The study of the properties of Æmilia specifications can be conducted in TwoTowers through equivalence verification with diagnostics, symbolic model checking with diagnostics via NuSMV 2.2.5, information flow analysis with diagnostics, reward Markov chain solution, and discrete event simulation.

Version 5.1 is being distributed since January 2006 both for Linux and for Windows. You can find a brief though complete description of the software tool in the first chapter (4 pages) of its user manual.

HOW TO GET A COPY OF THE TOOL

TwoTowers is distributed free of charge only to educational and non-profit organizations. In order to get the software tool, all you have to do is to download, fill in and sign the license agreement, then mail a scanned copy of it in PDF format to Marco Bernardo.

HOW TO INSTALL AND RUN THE TOOL

You can find the related instructions in the second chapter (4 pages) of the user manual both for Linux and for Windows.

EXAMPLES AND CASE STUDIES