Model Checking

Model checking allows us to verify if the model has a certain property or not. When it does not, usually the model is modified manually. We investigate methods so that such modification (update) can be performed mechanically. Verification is also applied to the study and modelling of genetic network, and to embedded systems for program verification.

Project listing:

Model Updating

Model Updating

Model checking provides the ability to verify if the model of a given system has a certain property or not. When it does not, usually the model is modified manually. In this line of research, we investigate methods so that such type of modifications ("update") are performed mechanically. Currently, we have an update method suitable for small models, and we think it is important to extend our technique to large systems with "symbolic" methods. It is also possible that our method has applications in "Incremental" Verification.
Genetic Network Construction using Model Verification

Genetic Network Construction using Model Verification

Currently, model checking is mostly used to design digital circuits. The resemblance between this type of circuits and Genetic Networks has allowed us to use a model checker as an auxiliary tool in the construction of Boolean Genetic Networks. We already have a first version of a system called "Antelope" , which we plan to extend to make it a more practical system.
raz
Application in Embedded Systems

Application in Embedded Systems

Usually the models that are verified with these techniques are finite, which is a problem for its application in ordinary software (that typically represent infinite models). We have avoided this difficulty by focusing on software to control embedded systems, specified with sets of finite machines. As a result, we were able to apply existing techniques for Model Verification in program verification. However, to date we have only verified small systems. We intend to move on to larger systems. This is a joint work with Vladimir Estivill-Castro.