This paper concerns the application of formal methods to biological systems, modeled specifically in BioAmbients, a variant of the Mobile Ambients calculus. Following the semantic-based 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.
Abstract interpretation based verification of temporal properties for BioAmbients
GORI, ROBERTA;LEVI, FRANCESCA
2010-01-01
Abstract
This paper concerns the application of formal methods to biological systems, modeled specifically in BioAmbients, a variant of the Mobile Ambients calculus. Following the semantic-based 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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
