CARMA Eclipse plugin

This is an Eclipse plug-in developed for supporting specification and analysis of CAS in CARMA. In this plug-in, CARMA systems are specified by using an appropriate high-level language for designers of CAS, named the CARMA Specification Language. This is mapped to the process algebra, and hence will enable qualitative and quantitive analysis of CAS during system development by enabling a design workflow and analysis pathway. The intention of this high-level language is not to add to the expressiveness of CARMA, which we believe to be well-suited to capturing the behaviour of CAS, but rather to ease the task of modelling for users who are unfamiliar with process algebra and similar formal notations.

Satellite tools

Bus Data Visualiser

This is a tool developed to support the automatic derivation of patch-based models from real data (specifically, GPS measurements). The tool is based on an API made publicly available by Lothian Buses that allows developers to access live bus GPS data. It can be made to collect data, which is then stored in a database so that it can be visualised at any time. In addition, it is also able to visualise live data.

The visualisation tool is implemented as a web application in JavaScript using jQuery and Bootstrap, with a back-end NoSQL database using Node.js and MongoDB. The tool is currently available here. Documentation for installation procedure on a local machine is available at this link.


This is a tool that offers an efficient on-the-fly algorithm for model checking PCTL formulae including scalable mean field approximation. FlayFast is provided within jSAM framework.


CRNReducer provides algorithms for the exact reduction of ordinary differential equa- tions (ODEs) arising from chemical reaction networks with mass-action semantics. The tool currently supports CRNs given in the “.net” format generated with the well-established tool BioNetGen.

PALOMA Eclipse plugin

The PALOMA Eclipse plugin provides a fully-featured development environment for modelling with the recently proposed PALOMA process algebra. The plug-in consists of:

  • An editor for PALOMA models with syntax highlighting functions;
  • A simulator which supports population-level stochastic simulation of PALOMA models using Gillespie’s algorithm;
  • Plotting facilities for simulation results;
  • A generator which can translate a PALOMA model to directly runnable Matlab scripts for moment-closure analysis using ODEs [FHG].

The source code of the plug-in is available here. A user manual about how to install and use the plug-in can be found at this link. Once the plug-in is installed, one can create a PALOMA model, parse it and then do time-series analysis of the model by stochastic simulation and moment-closure approximation. In the following we show the typical workflow supported by the tool.

Topochecker: a topological model checker

Topochecker is a spatio-temporal model checker based on closure spaces and Kripke frames. Currently it checks a spatial extension of CTL named STLCS (spatio-temporal logic of closure spaces).
The current version of topochecker, given its prototypical nature, is available in source code form at github, where you can find more information, download the tool and experiment with it.