Tools

  • The CARMA Eclipse Plugin supports 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.
    • The CARMA Eclipse Plugin is available from https://quanticol.github.io

  • The CARMA Graphical Plugin provides the user with tools for graphical modelling of space and movement in CARMA.
    • The graphical representation of the model, consisting of components, locations and paths laid out on a plane, is used for the automatic generation of CARMA code file.
    • The CARMA Graphical Plugin is available from https://quanticol.github.io

  • The CARMA Command-Line Interface offers an alternative to the Eclipse plugin for performing simulation experiments.
    • Simulations can be run without a graphical interface and make use of multi-core architectures. Multiple experiments can be executed sequentially, automating the process.
    • Results are stored in comma-separated value format, and the produced output also includes information about the simulation time and experiment performed, as well as a script to facilitate plotting of the results.
    • The CARMA Command-line simulator is available from https://quanticol.github.io 

  • The QUANTICOL Bus Simulator supports 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 QUANTICOL Bus Simulator is hosted at http://pepa.inf.ed.ac.uk:3000/

  • FlyFast offers an efficient on-the-fly algorithm for model checking PCTL formulae including scalable mean field approximation.
  • ERODE is a software tool for the solution and exact reduction of systems of ordinary differential equations (ODEs).
    • The tool supports two recently introduced, complementary, equivalence relations over ODE variables: forward differential equivalence partitions ODE variables into blocks for which a self-consistent aggregate ODE system can be obtained; each aggregate ODE gives the cumulative dynamics of the sum of the original variables in the respective equivalence class. Backward differential equivalence identifies variables that have identical solutions whenever starting from the same initial conditions.
    • ERODE uses a backend based on the well-known Z3 SMT solver to compute the coarsest equivalence that refines a given initial partition. In the special case of ODEs with polynomial derivatives of degree at most two, covering elementary chemical reaction networks (CRNs) and continuous time Markov chains (CTMCs), it implements a more efficient partition-refinement algorithm.
    • It is available from http://sysma.imtlucca.it/tools/erode/

  • 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.
    • The source code of the plug-in is available at https://github.com/cfeng783/paloma. A user manual about how to install and use the plug-in can be found at http://groups.inf.ed.ac.uk/paloma/usermanual.pdf. 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.

  • Topochecker is a spatio-temporal model checker based on closure spaces and Kripke frames. 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 https://github.com/vincenzoml/topochecker, where you can find more information, download the tool and experiment with it.

  • The jSSTL Eclipse plug-in is a Java tool for the specification and verification of Signal Spatio-Temporal Logic (SSTL) formulae. This tool, developed in Java, consists of a Java library (jSSTL API) and a front-end, integrated in Eclipse.  The jSSTL Eclipse plug-in is available from http://quanticol.sourceforge.net/?page_id=90

Please see the relevant pages for more information on how to use these tools.