FORMAL FRAMEWORK FOR THE ANALYSIS OF BIOLOGICAL REGULATORY NETWORKS USING PROMELA

Abstract

In the field of system biology, the study of regulatory networks leads biologists to the development of increasingly large, detailed and complex models. These complex models, replicating the dynamics of cell processes, are then analyzed using different approaches to obtain large amount of predictions. One such approach is simulation based analysis, which is extensively used for different predictions such as: how the concentration of a group of biological entities is varying in physiological conditions with respect to time. The major issue which subject to the limitation of simulation based analysis is; how to find interesting predictions about molecular mechanisms which control cellular processes, and how these predictions can be confronted with experimental data. In the last two decades formal verification has emerged as an important technique for the formal modeling and analysis of real time reactive and unpredictable systems in almost every field of science and engineering. The main advantage of model checking over simulation based analysis is its inherent soundness and reliability of computed results. Formal verification techniques based on model-checking provide us a powerful grounds to keep up with this increase in scale and complexity of the real time systems. The basic idea underlying model checking is to specify dynamical properties of interest as statements in temporal logic, and to use model-checking algorithms to automatically and efficiently verify whether the properties are satisfied or not by the model.