Edited Books & Journal Issues

Vol 51 (1), FMSD, 2017

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


                                  

        

IoT4CPS: Trustworthy IoT for CPS (2017-2020)




 

Project Description


IoT4CPS will develop guidelines, methods and tools to enable safe and secure IoT-based applications for automated driving and for smart production. The project will address safety and security aspects in a holistic approach both along the specific value chains and the product life cycles. To ensure the outreach of the project activities and results, the relevant stakeholders will be involved throughout the project and results will be disseminated to expert groups and standardization bodies. IoT4CPS will support digitalization along the entire product lifecycle, leading to a time-to-market acceleration for connected and autonomous vehicles. IoT4CPS will provide innovative components, leading to efficiency increases for the deployment of autonomous driving functions and in smart production environments, which will be validated in a vehicle and in a smart production demonstrator.


Partners:


Austrian Institute of Technology (National Coordinator), TU Wien, Institute of Science and Technology (IST), AVL List GmbH , Donau Uni Krems, Infineon Technologies AG, JKU Linz, Joanneum, NOKIA Österreich, NXP, Salzburg Research, SBA Research, SCCH, Siemens Aktiengesellschaft Österreich, TTTech Computertechnik AG, TU Graz, X-Net Services GmbH.

Contact Persons:

Ezio Bartocci (Project Leader for TU Wien), Radu Grosu, Muhammad Shafique

Research Team:

Ezio Bartocci, Radu Grosu, Faiq Khalid, Denise Ratasich, Muhammad Shafique

Funding:

 The Austrian Research Promotion Agency (FFG)
 



“SHiNE” - Systematic methods in systems engineering


II Period of the National Research Network “RiSE” (2015-2019)



     

Project Description


RiSE is an FWF-funded Research Network that bundles the research in formal verification in Austria. Fifteen researchers collaborate to move from a-posteriori verification to supporting programmers by computer-aided methods and tools that are based on a rigorous foundation.


My Task Description:

 

The goal of my task is to provide a formal-methods-based framework to perform rigorous analysis of timed systems with delays, faults and spatial distribution (networked).


Principal Investigators:


E. Bartocci, A. Biere, R. Bloem, C. Krishnendu, U. Egly, R. Grosu, T. Henzinger, C. Kirsch, L. Kovacs, U. Schmid, M. Seidl, A. Sokolova, H. Veith, G. Weissenbacher, F. Zuleger.

Website:

  ARISE

Funding:

 The Austrian Science Fund (FWF)
 
 


A framework for assertion based monitoring of automotive
systems-of-systems with mixed criticality (2014-2017)


Project Description



HARMONIA will 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 design process.


Principal Investigators:


E. Bartocci, T. Nguyen, D. Nickovic, R. Grosu

PhD Students:

K. Selyunin, S. Jaksic

Website:

 http://harmonia.vmars.tuwien.ac.at/

Funding:

 The Austrian Research Promotion Agency (FFG)


ICT COST Action IC1402 on Runtime Verification beyond Monitoring (ARVI) (2014-2018)


Project Description



Runtime verification (RV) is a computing analysis paradigm based on observing a system at runtime to check its expected behavior. RV has emerged in recent years as a practical application of formal verification, and a less ad-hoc approach to conventional testing by building monitors from formal specifications. There is a great potential applicability of RV beyond software reliability, if one allows monitors to interact back with the observed system, and generalizes to new domains beyond computers programs (like hardware, devices, cloud computing and even human centric systems). Given the European leadership in computer based industries, novel applications of RV to these areas can have an enormous impact in terms of the new class of designs enabled and their reliability and cost effectiveness. This Action aims to build expertise by putting together active researchers in different aspects of runtime verification, and meeting with experts from potential application disciplines. The main goal is to overcome the fragmentation of RV research by (1) the design of common input formats for tool cooperation and comparison; (2) the evaluation of different tools, building a growing sets benchmarks and running tool competitions; and (3) by designing a road-map and grand challenges extracted from application domains.


Management Committee:


E. Bartocci, T. Vojnar, J. Kofron, B. Nielsen, T. Uustalu, Y. Falcone, B. Jakimovski, B. Finkbeiner, K. Nakata, P. Stefaneas, A. Kakarountas, R. Unnthorsson, M. Kyas, B. Lee, N. Cardozo, S. Tyszberowicz, D. Peled, L. Mariani, Ferruccio Damiani, R. Seinauskas, J. Pang, M. Ouedraogo, G. J. Pace, C. Colombo, J. A. Perez, V. Stolz, M. Steffen, J. Rufino, J. Lourenco, Z. Budimac, C. Sanchez, J. Tapiador, G. Schneider, E. Zalinescu, N. Sharygina, G. Reger.

Websites:

 https://www.cost-arvi.eu/,  EU COST ARVI

Funding:

 European Cooperation in Science and Technology


ICT COST Action IC1405 on Reversible computation - extending horizons of computing (2015-2019)


Project Description



Reversible computation is an emerging paradigm that extends the standard forwards-only mode of computation with the ability to execute in reverse, so that computation can run backwards as naturally as it can go forwards. It aims to deliver novel computing devices and software, and to enhance traditional systems by equipping them with reversibility. The potential benefits include the design of revolutionary reversible logic gates and circuits - leading to low-power computing and innovative hardware for green ICT, and new conceptual frameworks, language abstractions and software tools for reliable and recovery oriented distributed systems. Landauer's Principle, a theoretical explanation why a significant proportion of electrical power consumed by current forwards-only computers is lost in the form of heat, and why making computation reversible is necessary and beneficial, has only been shown empirically in 2012. Hence now is the right time to launch a COST Action on reversible computation. The Action will establish the first European (and the world first) network of excellence to coordinate research on reversible computation. Many fundamental challenges cannot be solved currently by partitioned and uncoordinated research, so a collaborative effort of European expertise with an industrial participation, as proposed by this Action, is the most logical and efficient way to proceed.


Management Committee:


E. Bartocci, A. De Vos, P. Trancoso, A. Philippou, U. P. Schultz, R. Glueck, J. Kari, J. Krivine, J. Stefani, R. Wille, T. Worsch, P. Stefaneas, L. Aceto, A. Ingolfsdottir, M. Hennessy, M. Schellekens, I. Lanese, C. A. Mezzina, J. F. Groote, R. Schlatte, P. Kerntopf, M. Rawsky, C. Ferreira, A. Cunha, G. Ciobanu, D. F. Sburlan, R. Stankovic, S. Jaksic, T. Kapus, M. Kapus-Kolar, C. Moraga Roco, M. R. Mousavi, V. Gaspes, I. Phillips.

Websites:

 EU COST ARVI

Funding:

 European Cooperation in Science and Technology


Doctoral Program Logical Methods in Computer Science


Project Description



The LogiCS doctoral program is a PhD degree program funded by the Austrian Science Fund FWF and run jointly by the three Austrian universities Vienna University of Technology, Graz University of Technology and Johannes Kepler University Linz. This program is aimed at highly motivated students who want to work in one of three fundamental fields of computer science: Logic is a powerful reasoning tool. Originally invented as an aid for sound argumentation, it reached maturity in the form of mathematical logic and analytic philosophy in the early 20th century, with significant contributions from Vienna. We continue this tradition, using logic as a tool that enables computer programs to reason about the world. These reasoning tasks allow a natural classification into two broad areas: In Databases and Artificial Intelligence, logic is used to model, store, analyze and predict information about the outside world including the Internet. In Verification, logic is used to model, analyze and construct computer programs themselves. The logical and algorithmic questions which underlie both application areas are studied in the area of Computational Logic.


Faculty Members:

M. Baaz, A. Biere, R. Bloem, A. Ciabattoni, U. Egly, T. Eiter, C. Fermuller, R. Grosu, A. Leitch, M. Ortiz, R. Pichler, S. Szeider, H. Tompits, H. Veith, G. Weissenbacher.


Associated Faculty Members:

E. Bartocci, G. Gottlob, S. Hetzl, L. Kovacs, N. Musliu, G. Salzer, M. Seidl, M. Simkus, D. Weller, J. Widder, S. Woltran, F. Zuleger.


PhD Students:

A. Rodionova, A. Lukina

Websites:

 Logics.at

Funding:

 The Austrian Science Fund (FWF)


Doctoral College in Cyber-Physical Production Systems




Project Description



Production systems are extensively equipped with sensors, actuators and controllers, and the automation pyramid is linked through a communication network into an either strictly centralized or to a strictly decentralized IT structure. A fixed set of products and services is typically offered, and their realization is carefully planned in advance: Unfortunately, too sequential, too comprehensive, and hardware/product specific. Akin to a biological system, a CPPS will adapt itself in real time to its environment, reshape on the fly its products and production lines, and lower its costs and pollution footprint. While many advances are already under way, there are still many research and technological challenges that have to be mastered. One of the greatest challenges is to efficiently predict the emergent behaviors of these systems. However, the complexity of their models often hinders any attempt to exhaustively verify their safe behavior. An alternative method is to equip them with smart controller to predict emergent behaviors at runtime. This approach makes Cyber-Physical Systems self-aware opening up new perspectives to design smart systems able to dynamically self-organize or reconfigure themselves in order to adapt to the different circumstances.




PhD Student:

Guodong Wang

Website:

 Smart Attributes for CPPS

Funding:

 TU Wien


CyberHeart (2014-2018)




Project Description



The CyberHeart project is part of the NSF’s initiative to advance the state-of-the-art in Cyber-Physical Systems (CPS): engineered systems that are built from, and depend upon, the seamless integration of computation and physical components. The goal of this project is to develop far more realistic cardiac device models and controllers than the ones that currently exist. The CyberHeart platform will provide a basis to test and validate medical devices faster and at a far lower cost than existing methods. It will also provide a platform for designing optimal, patient-specific device therapies, thereby lowering the risk to the patient. CybeHeart includes collaborators from seven leading universities and centers CMU, RIT, UM, GTech, UPenn, FC-ESE, SBU, TUW and FDA.


Partners:

Carnegie Mellon University, University of Maryland, Stony Brook University, Georgia Tech, Rochester Institute of Technology, University of Pennsylvania, Fraunhofer Center for Experimental Software Engineering, Food and Drug Administration (FDA)

PhD Students:

Anna Lukina, Alena Rodionova

Website:

 CyberHeart

Funding:

 USA-NSF-CPS Frontiers


FCLOSE (2014-2017)




Project Description



Sharing services, data, and other resources are widespread in several application domains (e.g. storing and managing medical data across different health-care public and private organizations). A solution for such requirements comes from federated or hybrid cloud systems. However, ensuring data reliability and security in these systems becomes challenging, and classical solutions often bring some security limitations. For example, in classical cloud storage systems, data reliability techniques are transparent to the user, but the service provider is able to access the whole user dataset. As a consequence, reliability and security issues must be faced at different abstraction layers (e.g. data-link, application, …) according to different cloud delivery models (SaaS, PaaS, IaaS). They can be faced at design-time (adopting algorithms and techniques to verify reliability and security requirements) or at run-time (including monitors enforcing reliability and security properties). The target of this project is twofold: first, data coding, encryption and fragmentation techniques, as well as security protocols for federated and hybrid cloud storage will be designed and verified, starting from the low-level data manipulation techniques up to the optimization of the system design under reliability and security constraints. Second, such techniques will be applied to storage services for sensitive medical data.


Partners:

Università Politecnica delle Marche, TU Wien

Project members:

Marco Baldi, Ezio Bartocci, Franco Chiaraluce, Alessandro Cucchiarelli, Fabrizio Francescangeli, Gioele Luchetti, Fabrizio Marinelli, Giacomo Ricciutelli, Davide Schipani, Linda Senigagliesi, Luca Spalazzi, Francesco Spegni, Mirco Sturari, Primo Zingaretti

Website:

 FCLOSE