Welcome to Ellis Solaiman's page

I am a Teaching Fellow at the School of Computing Scince at Newcastle University. Details about subjects I teach can be found here.

My research interests are in the areas of: Software verification technologies, specifically model checking, modelling of business processes, representation and verification of electronic contracts and service level agreements, and recently technology enhanced learning.

This a list of some of the recearch projects I've been involved in recently:

Tools

• The Contract Complinace Checker (conch): Is a middleware tool for monitoring contract regulated business interactions--we call it the Contract Compliance Checker. The first version was implemented by Massimo Strano (a PhD student at th,at time supervised by Santosh Shrivastava) in Jboss Drools 4.0. The current version of the CCC is a major upgrade implemented by Ioannis Sfyrakis during his Advanced MSc project (a current PHD student in the school) supervised by Ellis Solaiman, and Carlos Molina.

  A copy of the source code is available from GitHub under the Apache Licence Version 2.0. Find it under the name of carlos-molina/conch project. Feel free to clone the project and give it a run. Feedback is very welcome.

• BPMNverifier (mosco): is a tool that can be used for mechanically verifying the logical correctness of choreography diagrams written in BPMN (Business Process Model Notation). It is a tool implemented in Java by Wenzhong Sun (Jim) -- an Advanced MSc students, supervised by Ellis Solaiman, and Carlos Molina. It can mechanically translate choreographies expressed in BPMN to Promela code, also allowing for automatic inclusion and verification of typical business correctness properties (in Linear Temporal Logic) using the Spin model checker.

  A copy of the source code is available from GitHub under the Apache Licence Version 2.0. Find it under the name of carlos-molina/mosco project.

  Feel free to clone the project and give it a run.

• EPROMELA: is a tool for modelling business contracts and verifying their logical correctness. The tool was built by Abubkr A. Abdelsadiq (a PhD student) supervised by Santosh Shrivastava, and Carlos Molina using the Spin model checker and its Promela input language.

  A copy of the source code is available from GitHub under the Apache Licence Version 2.0. Find it under the name of carlos-molina/contraval project.

• Design and Implementation of a BPMNtoPROMELA Translator, MSc Dissertation Project, Aug 2012.

  This MSc Dissertation was by Wenzhong Sun (Jim), and supervised by Ellis Solaiman and Carlos Molina-Jimenez and describes version 1.0 of BPMN2PROMELA in 62 pages.

• Deployment of the BPMN Verifier: User's Guide, Carlos Molina-Jimenez and Wenzhong Sun (Jim), Jan 2013. This document explains how to dowload, deploy and launch the BPMNverifier.
• Implementing a Contract Compliance Checker for Monitoring Contracts, MSc Dissertation Project, Aug 2012.

  This was a MSc dissertation project by Ioannis Sfyrakis, and supervised by Ellis Solaiman and Carlos Molina-Jimenez. It is a 50-page document that describes the Contract Compliance Checker.

• Deployment of the Contract Compliant Checker: User's Guide, Carlos Molina-Jimenez and Ioannis Sfyrakis, Jan 2013. This User's Guide explains how to dowload, deploy and launch the Contract Compliance Checker.