This paper concerns the application of formalmethods to biological systems, modeledspecifically in BioAmbients, a variant of the Mobile Ambients calculus. Following the semanticbased approach of abstract interpretation, we define a new static analysis that computes an abstract transition system. Our analysis has two main advantages with respect to the analyses appearing in the literature: (i) it is able to address temporal properties which are more general than invariant properties; (ii) it supports, by means of a particular labeling discipline, the validation of systems where several copies of an ambient may appear. We also design new weaker and more efficient analyses by means of simple widening operators. © 2010 Elsevier Inc. All rights reserved.
Gori, R., & Levi, F. (2010). Abstract interpretation based verification of temporal properties for BioAmbients. Information and Computation, 208(8), 869–921. https://doi.org/10.1016/j.ic.2010.03.004