6-8 juin 2017 Fréjus (France)
Modelling and Formal Verification of Neuronal Archetypes Coupling
Elisabetta De Maria  1@  , Thibaud L'yvonnet  1@  , Alexandre Muzy  1@  , Franck Grammont  2@  , Daniel Gaffé  3@  , Annie Ressouche  4@  
1 : I3S
Université de Nice Sophia-Antipolis
2 : LJAD
Université de Nice Sophia-Antipolis
3 : LEAT
Université de Nice Sophia-Antipolis
4 : INRIA
Université de Nice Sophia-Antipolis

There exists many ways to connect two, three or more neurons together to form different graphs. We call archetypes only the graphs whose properties can be associated with specific classes of
biologically relevant structures and behaviors. These archetypes are supposed to be the basis of typical instances of neuronal information processing. To model different representative archetypes
and express their temporal properties, we use a synchronous programming language dedicated to reactive systems (Lustre). The properties are automatically validated thanks to a model checker supporting data types (kind2). The language Lustre and the model checker kind2 are then exploited to investigate the behaviour of the composition of the presented archetypes.


Personnes connectées : 1