University of Twente
P.O. Box 217
7500 AE Enschede
Phone: +31 (0)53 489 3979
Fax: +31 (0)53 489 3247
Office: Zilverling 3122
Since 2016 my research work has extended to the fields of security,
safety, and their integration. I currently work in the European project
SUCCESS, which applies formal
analysis and validation techniques with the aim of successfully employing
IoT (Internet of Things) technologies in the healthcare sector.
Modeling and analysis are integrated in the planning and validation of
application scenarios and smart-device architectures, to address burning
security issues like unintentional or intentional insider attacks.
I have also been involved in projects focusing on the (cyber-) security of critical systems, and its relation to safety procedures. Security countermeasures are often intended to make a system less accessible, but for safety reasons some parts of a system (e.g. escape routes) must remain accessible at all times. We study the ways in which security and safety can collide with each other, with the aim of making a framework that can account for both at the same time. This will allow to have a better picture of the system, helping policymakers with their choices.
Between 2010 and 2016 I have been working on modelling biological pathways with Timed Automata. The project aims at producing a framework to quantitatively model the interactions occurring inside biological cells. In particular, we have been focusing on the dynamic evolution of kinase pathways, which are the mechanisms underlying the cellular response to external signals such as growth and death factors. The modelling tool ANIMO (Analysis of Networks with Interactive Modelling) is the result of a collaboration with biologists and experts in human-machine interaction. The formal foundation of the framework rests on Timed Automata, and models are checked against experimental data thanks to the powerful tool UPPAAL. The Timed Automata formalism is hidden behind a user interface based on Cytoscape, a widely spread program used in modeling biological interactions. This makes it easy for the molecular biologist to test and formulate hypotheses about a specific kinase network without needing any knowledge about the underlying formal model.