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
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.
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
You can find the related instructions in the second chapter (4 pages) of the user
manual both for Linux and for Windows.