The application of formal methods to the examination of reactive programs simulating cell systems’ behaviours in current computational biology is taken to shed new light on the simulative approaches in Artificial Intelligence and Artificial Life. First, it is underlined how reactive programs simulating many cell systems’ behaviours are more profitably examined by means of executable models of the simulating program’s executions. Those models turn out to be representations of both the simulating reactive program and of the simulated cell system. Secondly, it is highlighted how discovery processes of significant regular behaviours of the simulated system are carried out performing algorithmic verifications on the formal model representing the biological phenomena of interest. Finally, a distinctive methodological trait of current computational biology is recognized in that the advanced model-based hypotheses are not corroborated or falsified by testing the simulative program, which is not even encoded, but rather by performing wet experiments aiming at the observation of behaviours corresponding to paths in the model either satisfying or violating the hypotheses under evaluation.
Keywords: Artificial life, Computer simulation, Executable biology, Model-Based reasoning, Model checking, Philosophy of computer science