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.
|Autori:||GORI R; F.LEVI|
|Titolo:||Abstract interpretation based verification of temporal properties for BioAmbients|
|Anno del prodotto:||2010|
|Digital Object Identifier (DOI):||10.1016/j.ic.2010.03.004|
|Appare nelle tipologie:||1.1 Articolo in rivista|