Graphical User Interface: Main window

Welcome to the home page.

(written ETMCC) is a prototype implementation of a model checker for continuous time Markov chains: Requirements specified in the Continuous Stochastic Logic (CSL) are checked against a labelled continuous-time Markov chain. In addition to CTL-type model checking algorithms, includes sophisticated numerical analysis techniques which enable the tool to answer questions such as:

"Is there at least a 95% chance that the sending of a message will be confirmed by an acknowledgement within 50 ms?".

is developed by the Stochastic Modeling and Verification group at the University of Erlangen-Nürnberg, Germany, and the Formal Methods group at the University of Twente, the Netherlands.

For a motivation and a short introduction to the tool architecture visit the overview page. A closer look into the algorithms used by as well as case studies are presented in the tool papers on the publications page.

is free for non-profit organizations. However, the user has to fill in a license agreement before downloading and using the tool. A small user's guide (also part of the distribution) for installing and using the tool is available here.

The current version of is our second release (version 1.4). We are working on improvements concerning stability, speed and accuracy. This version comes along with an experimental model checking engine that supports verification techniques to check aCSL (action based CSL) requirements against action-labelled continuous time Markov chains.

Please feel free to email us with any bug reports, queries or comments.