TwoTowers is 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 checking 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.
Tool papers: FORTE/PSTV 1998, PERFORMANCE TOOLS 2000, MASCOTS 2003, QEST 2004.
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 send via email a copy of it in PDF format to Marco Bernardo.
You can find the related instructions in the second chapter (4 pages) of the user manual both for Linux and for Windows.