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.
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.
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.
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.