A Formal Model for the Simulation and Analysis of Early Biofilm Formation

Abstract

Biofilms are structured communities of bacterial cells adher ent to a surface. This bacterial state is called sessile. This paper focuses on the modelling of the transition between plank tonic and sessile state using Real-time Maude as the modelling language. With more and more bacteria joining the sessile community, the likeli hood of producing a biofilm increases. Once the percentage of bacterial cells that adheres to the surface reaches a threshold, which is specific for the considered bacterium species, a permanent biofilm is formed. An important challenge is to predict the time needed for the formation of a biofilm on a specific surface, in order to plan when the material infras tructure that comprises such a surface needs to be cleaned or replaced. We exploit the model-checking features of Real-time Maude to formally prove that a regular cleaning or replacement of the infrastructure pre vents the biofilm formation.