Software verification of biomolecular systems

This chapter describes the kinetics of the sodium-potassium exchange pump in terms of the pi-calculus process algebra. The pi-calculus has the advantage of a software verification tool. We emphasize that this software tool is able to check various properties and to provide confidence in the formal description of the pump. This model checker is used to verify that our model of the pump is deadlock free. It is also used to prove that a detailed description with a large number of states has the same behaviour with a model with a smaller number of states. This simpler model can become a part of a larger system, and in this way we get a scalable and compositional abstraction for biomolecular systems.