Edited Books & Journal Issues

Special Issue on Runtime Verification, FMSD, 2017 (coming soon)

LNBI Vol. 9859, CMSB 2016

Vol. 4, STTT 2016

LNCS Vol. 9333, RV 2015

Vol. 236, Inf & Comp 2014

LNCS Vol. 7976, SPIN 2013

News about me !!

March 2015 - Rigorous Systems Engineering continues to rise and shine


December 2014 - "Laufbahnstelle" for Ezio Bartocci


January 2014 - Habilitation as Associate Professor in Italy


March-April 2013 - My GPU simulations featured on Cover of Transactions on Computational Biology and Bioinformatics


Nov. 2011 - Post Doc of the Month (Interview)


Sep. 2011 - Best Paper Award (RV 2011)


July 2011 - From chaos to cures (Cornell University)


Jan. 2011 - CMACS Researchers Perform First Automated Formal Analysis of Realistic Cardiac Cell Model


UNICAM news:

Counter and browser compatibility



Get Firefox!


Get Thunderbird!


Valid XHTML 1.0 Transitional



Hardware Monitoring for Automotive Systems-of-Systems


The verification of complex mixed-signal integrated circuit products in the automotive industry accounts for around 60%-70% of the total development time. In such scenario, any effort to reduce the design and verification costs and to improve the time-to-market and the product quality will play an important role to boost up the competitiveness of the automotive industry. The aim of the HARMONIA project is to provide a framework for assertion-based monitoring of automotive systems-of-systems with mixed criticality. It will enable a uniform way to reason about both safety-critical correctness and non-critical robustness properties of such systems. Observers embedded on FPGA hardware will be generated from assertions, and used for monitoring automotive designs emulated on hardware. The project outcome will improve the competitiveness of the automotive application oriented nano and microelectronics industry by reducing verification time and cost in the development process.

[1] Ezio Bartocci, Radu Grosu, Stefan Jaksic, Thang Nguyen, Dejan Nickovic, Konstantin Selyunin, The HARMONIA project: Hardware Monitoring for Automotive Systems-of-Systems, In Proc. of ISoLA 2016, the 7th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, 2016, Springer
[2] Stefan Jaksic, Ezio Bartocci, Radu Grosu, Reinhard Kloibhofer, Thang Nguyen, Dejan Nickovic: From Signal Temporal Logic to FPGA monitors, In Proc. of MEMOCODE 2106: the 13th {ACM/IEEE} International Conference on Formal Methods and Models for Codesign, 2016, ACM
[3] Stefan Jaksic, Ezio Bartocci, Radu Grosu, Dejan Nickovic, Quantitative Monitoring of STL with Edit Distance, In Proc. of RV 2016: the 7th International Conference on Runtime Verification, Springer, Lecture Notes in Computer Science, 2016, to appear
[4] Konstantin Selyunin, Thang Nguyen, Ezio Bartocci, Dejan Nickovic, Radu Grosu, Monitoring of MTL Specifications With IBM's Spiking-Neuron Model, In Proc. of the 2016 Design, Automation & Test in Europe Conference & Exhibition, IEEE Computer Society, pp. 924-929, 2016
[5] Alena Rodionova, Ezio Bartocci, Dejan Nickovic, Radu Grosu, Monitoring of MTL Specifications With IBM's Spiking-Neuron Model, Temporal Logic as Filtering, In Proc. of HSCC 2016: the 19th International Conference on Hybrid Systems: Computation and Control pp. 11-20, 2016, ACM

Ezio Bartocci (TU Wien), Konstantin Selyunin (TU Wien), Thang Nguyen (Infineon)



Neural Programming: Towards Adaptive Control in Cyber-Physical Systems


We introduce Neural Programming (NP), a novel paradigm for writing adaptive controllers for Cyber-Physical Systems (CPSs). In NP, if and while statements, whose discontinuity is responsible for frailness in CPS design and implementation, are replaced with their smooth (probabilistic) neural nif and nwhile counterparts. This allows one to write robust and adaptive CPS controllers as dynamic neural networks (DNN). Moreover, with NP, one can relate the thresholds occurring in soft decisions with a Gaussian Bayesian network (GBN). We provide a technique for learning these GBNs using available domain knowledge. We demonstrate the utility of NP on three case studies: an adaptive controller for the parallel parking of a Pioneer rover; the neural circuit for tap withdrawal in C. elegans; and a neural-circuit encoding of parallel parking which corresponds to a proportional controller. To the best of our knowledge, NP is the first programming paradigm linking neural networks (artificial or biological) to programs in a way that explicitly highlights a program's neural-network structure.

[1] K. Selyunin, D. Ratasich, E. Bartocci, Md. A. Islam, S. A. Smolka, R. Grosu: Neural Programming: Towards adaptive control in Cyber-Physical Systems. In Proc. of CDC 2015, the 54th IEEE Conference on Decision and Control, 2014, pp. 6978-6985, IEEE

Neural Program for Automatic Parking: Normal Tires Neural Program for Automatic Parking: Wet Tires

GPU-based real-time simulation of cardiac dynamics


Real-time simulation refers to the ability to execute a computer model of a physical system at the same rate as the actual physical system. Recently, the advantages of GPU over CPU processing have been established for many areas of science, including systems biology. Using the CUDA (Compute Unified Device Architecture) parallel programming model from NVIDIA, the highly parallel and multi-core capabilities of GPUs can be exploited to achieve extremely fast simulations of complex models in 2D and 3D. If such large-scale realistic models can be simulated in near real-time, many more applications, including patient-specific treatment strategies for cardiac-rhythm disorders, become feasible without the need for supercomputers. To date, such efforts have come up short.

[1] E. Bartocci, E. M. Cherry, J. Glimm, R. Grosu, S. A. Smolka, Flavio Fenton. Toward Realtime Simulation of Cardiac Dynamics. In Proc. of CMSB'11, the 9th International Conference on Computational Methods and Systems Biology, Paris, September 2011.
[2] E. Bartocci, R. Singh, F. von Stein, A. Amedome, Alan-Joseph Caceres, J. Castillo, E. Closser, G. Deards, A. Goltsev, R. Sta. Ines, C. Isbilir, J. Marc, D. Moore, D. Pardi, S. Sadhu, S. Sanchez, P. Sharma, A. Singh, J. Rogers, A. Wolinetz, T. Grosso-Applewhite, K. Zhao, A. Filipski, R. Gilmour Jr, R. Grosu, J. Glimm, S. A. Smolka, E. Cherry, E. Clarke, N. Griffeth, and F. Fenton. Teaching cardiac electrophysiology modeling to undergraduate students; using Java Applets and GPU programs to study arrhythmias and spiral wave dynamics.   Journal of Advances in Physiology of Education, vol. 35 no. 4, pag. 427-437. Full PDF

Difference in terms of performances between CPU computation (on the left Intel i7) and GPU computation (GPU Tesla C1060) of a 2D cardiac simulation of 512X512 elements running in parallel in the same machine. CUDA 3D Simulation of the Rabbit's Heart Ventricle Cardiac Dynamics.
Normal Wave propagation
(512x512 cells)
Spiral caused by a not excitable region
(512x512 cells)

In-silico analysis using workflow management systems


An in-silico experiment can be naturally specified as a workflow of activities implementing, in a standardized environment, the process of data and control analysis. A workflow has the advantage to be reproducible, traceable and compositional by reusing other workflows. In order to support the daily work of a bioscientist, several Workflow Management Systems (WMSs) have been proposed in bioinformatics. Generally, these systems centralize the workflow enactment and do not exploit standard process definition languages to describe, in order to be reusable, workflows. While almost all WMSs require heavy stand-alone applications to specify new workflows, only few of them provide a web-based process definition tool. We have developed BioWMS, a Workflow Management System to support the definition, the execution and the results management of an in-silico experiment through a web-based interface. BioWMS, implemented on BioAgent/Hermes architecture, generates dynamically domain-specific, agent-based workflow engines from a user workflow specification. Our approach exploits the proactiveness and mobility of agent-based technology to embed the application domain features inside agents behaviour. The resulting workflow engine is a multiagent system -a distributed, concurrent system- typically open, flexible, and adaptative.

Click here to watch the video of BioWMS



Computational models in systems biology



Systems biology is a multidisciplinary field whose goal is to provide a systems-level understanding of biological phenomena by uncovering their structure, dynamics and control methods. A main focus of systems biology is to devise mathematical or formal models that capture significant aspects of in vitro or in vivo experimental data, while remaining amenable to both quantitative and qualitative analysis. Currently, the most popular modeling approach is to use complex systems of nonlinear differential equations, describing in great detail the underlying biological phenomena. These models, however, are not particularly suitable for formal analysis, and impose high computational demands on simulation, especially in large-scale 2D and 3D networks. Simulation at the organ or even the cell level is thus rendered impractical. Considering this state of affairs, systems biology could greatly benefit from the development of techniques that given a system of nonlinear differential equations, (semi-automatically) constructs a more abstract model that preserves the properties of interest. One promising approach is based on the use of Hybrid Automata (HA) as a modeling formalism for complex biological processes. HA are an extension of finite automata that allows one to associate a continuous behavior with each state.



Simulation

I'm interested on efficent simulation techniques for biological systems. In particular we are developing a simulator, CellExcite, in order to reproduce in silico the emergent behavior of excitable tissues such as cardiac tissue. We can reproduce several phenomena such as fibrillation and defibrillation using a strong electric shock as the the following movies show.

Ventricolar Fibrillation
(Tissue of 400x400 cells)
Defibrillation
(Tissue of 400x400 cells)
ruler.gif


Spatial Model Checking

One of the most important and intriguing questions in systems biology is how to formally specify emergent behavior in biological tissue, and how to efficientlypredict and detect its onset. A prominent example of such behavior is electricalspiral waves in spatial networks of cardiac myocytes (heart cells). Spiral waves of this kind are a precursor to a variety of cardiac disturbances, including atrial fibrillation (AF), an abnormal rhythm originating in the upper chambers of the heart. Moreover, the likelihood of developing AF increases with age. In the paper [1], we addressed this question by proposing a simple and efficient method for learning and automatically detecting the onset of spiral waves in cardiac tissue. Underlying our method is a linear spatial-superposition logic (LSSL), which we have developed for specifying properties of spatial networks. Our method also builds upon hybrid-automata, image-processing, machine-learning and model-checking techniques to first learn an LSSL formula that characterizes such spirals. The resulting formula is then automatically checked against a quadtree (SQT) representation of the scalar electric field, produced by simulating a hybrid automata network modeling the myocytes, at each discrete time step. The SQT representation is obtained via hybrid abstraction and hierarchical superposition of the elementary units within the field.



[1] R. Grosu, E. Bartocci, F. Corradini, E. Entcheva, S.A. Smolka and A. Wasilewska. Learning and Detecting Emergent Behavior in Networks of Cardiac Myocytes. In Proc. of HSCC'08, the 11th International Conference on Hybrid Systems: Computation and Control, St. Louis, USA, April, 2008, pp. 229-243, Springer, LNCS 4981.