Postdoctoral positions at the GSSI on modelling and verification for cyber-physical and smart systems

The Computer Science group at the Gran Sasso Science Institute (GSSI, an international PhD school and centre for advanced studies located in L’Aquila, Italy) has two available postdoctoral positions on topics related to modelling and verification for cyber-physical and smart systems. The positions are in the context of two PRIN projects funded by the Italian Ministry for University and Research, namely "Designing Spatially Distributed Cyber-Physical Systems under Uncertainty (SEDUCE)" (Catia Trubiani, PI at the GSSI) and "IT MATTERS: Methods and Tools for Trustworthy Smart Systems" (Luca Aceto, PI at the GSSI). Each position is for two years and the salary is 36,000€ per year before taxes. The positions are renewable for a third year if this is mutually agreeable.

The positions are briefly described below. We foresee a close collaboration between the members of the teams working on the two projects. The application must be submitted through the online form available at https://applications.gssi.it/postdoc/ by Thursday, 11 July 2019 at 6 p.m. (Central European Time). For more information, please consult the Call for Applications at https://applications.gssi.it/postdoc/ or write an email to the PIs of the respective projects.

Note that the Computer Science group at the GSSI also has a further position financed by the institute, which can be filled in any of the research themes within the group. See http://cs.gssi.it for more information.

Requirements: Candidates are expected to have a PhD degree in Computer Science or related disciplines. Preference will be given to applicants who have previous research experience on topics related to the themes of the project.

Postdoctoral position within the project "Designing Spatially Distributed Cyber-Physical Systems under Uncertainty", supervised by Catia Trubiani: https://cs.gssi.it/catia.trubiani.

Brief description of the project: Emerging scenarios such as autonomous vehicles and the Internet-of-Things require large-scale cyber-physical systems (CPS), i.e., computing devices that interact with the physical world. To cope with their complexity, model-based design has long been advocated as a prominent approach for their rigorous development. However, the state of the art does not adequately account for two major issues: space, to capture the distribution of CPS devices as well as their mobility; and uncertainty, e.g., to reflect lack of knowledge about the environment, the accuracy of the model, or errors occurring in the real world. Our goal is to develop modelling and analysis techniques for CPS where space and uncertainty are first-class citizens. We envisage a component-based framework where digital and physical components have locality and mobility features, and where uncertainty is captured by means of probabilistically distributed activities to describe their dynamics. We devise a system to specify spatio-temporal CPS requirements, turning them into probabilistic spatio-temporal logical specifications that will be at the basis of efficient algorithms for the analysis, verification, and synthesis. We will apply our techniques to real case studies on smart buildings and crowd-navigating robots.

Main activities: The successful candidate will develop a component-based modelling language for the specification of cyber physical systems, where digital components (i.e., the computational devices), need to co-exist with physical components (i.e., the dynamical models of the physical world). Each component will feature an appropriate location and mobility model. Uncertainty will be specified with either probabilistically distributed activities, or nondeterministically, leading to reasoning that will take into account worst- and best-case scenarios under any possible value of such uncertain actions. The modelling framework will allow the specification of spatio-temporal requirements, which establish the behavioural guarantees to be satisfied by the CPS under analysis. The postdoctoral researcher will work with Catia Trubiani at the GSSI, and she/he will also collaborate with the project partners at IMT Lucca (Mirco Tribastone, coordinator of the project), University of Trieste (Luca Bortolussi and Stefano Seriani), and University of Camerino (Francesco Tiezzi).


Postdoctoral position within the project "IT MATTERS: Methods and Tools for Trustworthy Smart Systems" supervised by Luca Aceto: http://www.gssi.it/people/professors/lectures-computer-science/item/225-aceto-luca.

Brief description of the project: The goal of the project is the development and the application of a novel methodology for the specification, implementation and validation of trustworthy smart systems based on formal methods. We envisage system development in three steps by first providing and analysing system models to find design errors, then moving from models to executable code by translation into domain-specific programming languages and, finally, monitoring runtime execution to detect anomalous behaviours and to support systems in taking context-dependent decisions autonomously. Scientifically, the research will yield new, fundamental insights on the general properties of large scale, physically located, smart systems, leading to an end-to-end, principled approach to their design, implementation and deployment. The developed software tools and the work on the case studies will show the effectiveness of our proposed approach in three practical scenarios at different application scales.

Main activities: The successful candidate will develop runtime-monitoring and software-model-checking techniques for “smart systems”, that is, systems that take context-dependent decisions autonomously. The research activities will involve developing frameworks that can deal with the distributed nature of smart systems and will build on existing work on specification-based monitoring and software model checking of cyber-physical systems. The postdoctoral researcher will also devise techniques to use information derived from the runtime analysis to guide the software-model-checking effort and to refine the models of the runtime environment used in model checking. The postdoctoral researcher will work with Luca Aceto, Omar Inverso, Ludovico Iovino and Emilio Tuosto at the GSSI. He/she will also collaborate with the project partners at IMT Lucca, CNR Pisa, University of Camerino, University of Pisa and University of Udine. Moreover, he/she will also interact with the concurrency group at ICE-TCS (http://icetcs.ru.is/), Reykjavik University, led by Luca Aceto and Anna Ingólfsdóttir.