Modeling & Analysis in
Software Engineering

 About     |     Members     |     Research     |     Publications     |     Software     |     Contact Us



Some of the Software We Have Used or Are Using

  • aperiot: parser generator for Python
  • Concurrency Workbench (Edinburgh) (CWB): CCS equivalence analyses/model-checker
  • Mobility Workbench (MWB): pi-calculus/fusion-calculus equivalence analyses/model-checker
  • Failures-Divergence-Refinement (FDR): CSP model-checker
  • Construction and Analysis of Distributed Processes (CADP): LOTOS model-checker
  • MetaModel Coverage Checker (MMCC): tool for generating testcases for model transformations
  • Kermeta: language and environment for metamodel engineering (e.g., model transformation, execution, and analysis)
  • TXL: language for source code transformation
  • Alloy: A language and tool to describe and analyze object structures
  • MetaEdit+: A tool for domain-specific modeling and development
  • JPF: An explict-state model checker for Java
  • Spin: An explicit-state model checker for Promela
  • UppAal: A model checker for Timed Automata
  • NuSMV: A symbolic model checker
  • VeriSoft: A model checker for C/C++
  • Eclipse: An IDE for software development
  • IBM RSA-RTE: One of the best model-driven development tools around
  • kiltera: A high-level language for modeling and simulating concurrent, distributed, mobile, and timed systems
  • Jape: A highly customizable proof checker
  • Eclipse Modeling Framework (EMF): Software modeling with Eclipse
  • Graphical Modeling Framework (GMF): A tool for creating graphical editors automatically
  • LaTeX: a system for document preparation
  • Lego MindStorms: Robots for the masses
  • Java Emitter Templates (JET): A language for model-to-text transformation
  • ATL: A language for model-to-model transformation
  • ExMan: A customizable framework for mutation analysis
  • Choco: A constraint solver
  • IDES: A tool for Discrete Event Systems
  • Aglets: A language for Mobile Agents

Some of the Software We Have Written

Ernesto Posse

kiltera is a language for modelling and simulating concurrent, interacting, real-time processes, with support for mobility and distributed systems. kiltera can be downloaded here.

Symbolic Analysis of UML-RT Models (SAUML 0.0.1)
Karolina Zurowska, Juergen Dingel

An extension to the IBM RSA RTE that enables symbolic execution and analysis of UML-RT capsules. The plugins work for Windows 7 and IBM RSA RTE v. 7.5.2.

SAUML2 - a Verification Tool for UML-RT Models Based on Symbolic Analysis (SAUML2 0.1.1)
Karolina Zurowska, Juergen Dingel

An extension to the IBM RSA RTE that enables verification of properties of UML-RT models. The plugins work for Windows 7 and IBM RSA RTE v. 8.0.4.

ExMAn and ConMAn
Jeremy Bradbury, Jim Cordy, Juergen Dingel

ExMAn is an experimental mutation analysis framework supporting the comparative evaluation of different fault detection techniques such as model checking and testing using program mutation. The ExMAn is hosted here.
ConMAn is a set of 24 concurrency mutation operators for Java (J2SE 5.0). More information can be found here.

Embee and StateDumper Software
Juergen Dingel, Michelle Crane

Embee is a prototype runtime conformance checker for Java programs. Embee takes as input an Alloy specification (using a limited subset of the Alloy language) and a textual configuration file provided by the user. It creates several intermediate text files containing runtime information which are used to check the conformance a specific breakpoints. StateDumper is a separate, stand-alone program used by Embee that retrieves the runtime information from executing Java programs. It relies on classes and methods from the Java Platform Debugger Architecture (JPDA) from Sun Microsystems.

Verisoft Automatic Interface (VAI) Framework 
Juergen Dingel, Hongzhi Liang

VeriSoft is a software model checker developed at Bell Labs. It takes as input C/C++ programs in which concurrent processes communicate through either semaphores, channels, or shared memory. The VAI Framework works with Verisoft by providing the following wrapper tools:

  • VAI Front-End: Automatically transforms C/C++ IPC objects to VeriSoft IPC objects.
  • VAI Back-End: Provides a Java interface for paring a VeriSoft trace file and accessing its content

Financial support for the development of this software is provided by the Natural Sciences and Engineering Research Council of Canada (NSERC).


Software Technology Lab     |     School of Computing    |     Queen's University