The Shape Calculus is a bio-inspired timed and spatial calculus for describing 3D geometrical shapes moving in a space. Shapes, combined with a behaviour, form 3D processes, i.e., individual entities able to bind with other processes on compatible spatial channels and to split over previously established bonds. Due to geometrical space, timed behaviours, a wide degree of freedom in defining motion laws and usual nondeterminism, 3D processes typically exhibits an infinite behaviour that prevents any decidable analysis. Shape Calculus models are currently used only for simulation and, thus, validation of models and hypothesis testing. In this work we introduce a complementary, and synergetic, way of using the calculus for systems biology purposes: we define a first abstract interpretation that can be used to verify untimed and unspatial safety properties of a given model. Such an abstraction focuses on the possible interactions that, during the evolution of the system, can occur among processes yielding new composed processes and, thus, new species. Other possible abstract domains for the verification of more expressive properties are also discussed.

Towards Abstraction-Based Verification of Shape Calculus

BUTI, Federico;CALLISTO DE DONATO, Massimo;CORRADINI, Flavio;DI BERARDINI, Maria Rita;MERELLI, Emanuela;TESEI, Luca
2012-01-01

Abstract

The Shape Calculus is a bio-inspired timed and spatial calculus for describing 3D geometrical shapes moving in a space. Shapes, combined with a behaviour, form 3D processes, i.e., individual entities able to bind with other processes on compatible spatial channels and to split over previously established bonds. Due to geometrical space, timed behaviours, a wide degree of freedom in defining motion laws and usual nondeterminism, 3D processes typically exhibits an infinite behaviour that prevents any decidable analysis. Shape Calculus models are currently used only for simulation and, thus, validation of models and hypothesis testing. In this work we introduce a complementary, and synergetic, way of using the calculus for systems biology purposes: we define a first abstract interpretation that can be used to verify untimed and unspatial safety properties of a given model. Such an abstraction focuses on the possible interactions that, during the evolution of the system, can occur among processes yielding new composed processes and, thus, new species. Other possible abstract domains for the verification of more expressive properties are also discussed.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11581/243115
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? ND
social impact