Academic Journals Database
Disseminating quality controlled scientific knowledge

Modular Verification of Interactive Systems with an Application to Biology

ADD TO MY LIST
 
Author(s): P. Drabik | A. Maggiolo-Schettini | P. Milazzo

Journal: Scientific Annals of Computer Science
ISSN 1843-8121

Volume: 21;
Issue: 1;
Start page: 39;
Date: 2011;
VIEW PDF   PDF DOWNLOAD PDF   Download PDF Original page

ABSTRACT
We propose sync-programs, an automata-based formalism for the description of biological systems, and a modular verification technique for such a formalism that allows properties expressed in the universal fragment of CTL to be verified on suitably chosen fragments of models, rather than on whole models. As an application we show the modelling of the lac operon regulation process and the modular verification of some properties. Verification of properties is performed by using the NuSMV model checker and we show that by applying our modular verification technique we can verify properties in shorter times than those necessary to verify the same properties in the whole model.
RPA Switzerland

RPA Switzerland

Robotic process automation

    

Tango Jona
Tangokurs Rapperswil-Jona