What is CISMO ?
 

CISMO is a continuous state space model checker based on labeled Markov chain processes (LMP). Model checkers reduce the risk of catastrophes in real life situation by detecting logical errors in systems. A system may be a computer program or a representation of a machine's behavior. While traditionnal model checker are sufficient for basic theorical verification, they often prove to be insufficient for real life situations.

The major flaw plaguing regular model checker is that their state space is finite. While this may be adequate for some systems, a lot of systems depends on continuous factors, like the height for an elevator, the temperature for a heater or a quantity for a coffee maker. Cismo use LMP systems to represents reactive systems. A reactive system reacts to an external event (an action like pressing a button), and the states actually represents the factor to measure. For example, for a coffee maker, the states would represent the quantity of served coffee.

Cismo is also based on the asumption that nothing is 100% reliable. As such, every action on the system has a certain probability of being ineffective. For example, for a coffee maker, the fact that the user presses the button to serve a coffee is not guaranteed to produce an acceptable result. The user may have to press a second time in order to receive coffee. There may be several reasons explaining such unacceptable result, but they are not relevant to the quantity of coffee served. We want to abstract the reason of failure and only include it as a general probability.

Let's see the difference betweeen a LMP system and a traditionnal system also called an automat. This is a non deterministic automat representing a very simple coffee maker. Note that there is no final state, because the coffee maker must never stop to serve.

While this certainly looks good on paper, we have yet to find such a machine. When requesting a refund, there is a probability the coin will ge stuck inside the machine. We could have added probabilities for each action, but that would still not make the system better. It is absurd to believe that the machine will serve exactly 350 mL of coffee. The quantity will always somewhat vary, or the machine could be experiencing failure. Factors that cause variations in the quantity may be misplaced cup, water remaining in the tap, malfunctionning water quantity sensor, and so on. The following system can be verified by Cismo. While still not very accurate, it is still much better.

To create a model recognizable by Cismo, the states must be mapped onto a continuous factor. The obvious choice here is the quantity of coffee served. Two intervals are noteworthy : [200, 400] for a small coffee and ]400, 700] for a large coffee. There is also a discrete interval that is zero, meaning no coffee at all has been served. We will also add a second point that will be our starting state : 1000. Finally, a third point, 2000, will represent a system failure. Note that since Cismo does not recognize lambda transitions, we will have to adapt the system :

This system already represents a more realistic model. This machine can experience failure during payment or operations. The lambda operation has a 99% chance of success, meaning that the machine can get stuck after serving coffee. For more complete examples of systems that Cismo can verify, please see the "Examples" page.

Cismo is useful for checking high reliability systems and detrrmining if the failure rate is acceptable. The Cismo model checker has been designed by Nicolas Richard during the master degree at computer sciences department of Université Laval. MTBDDs data structures support has then been added by Simon Paquet. Finally, a random system generator as well as mostly bug fixes has been provided by Frédérick Lemay during summer 2005. Cismo is directed by Josée Desharnais, developped for the LSFM research group, at Université Laval.

Cismo is written in portable JAVA, except for the MTBDDs data structures, which are using the C library CUDD, currently only available for Linux. Every functions of Cismo using the standard hash tables structures are available for all operating systems. The use of MTBDDs can reduce the verification time by about 20% for complex systems.