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.
Mendeley saves you time finding and organizing research
Choose a citation style from the tabs below