Looking for case studies

Below is a list of research work looking for industrial case studies. If the item does not provide a contact person, contact the chairperson of WG4 for more information. (christian.colombo(a)um.edu.mt)


  • [cps] cyber-physical systems
  • [fin] for financial applications
  • [med] for medical applications
  • [con] for electronic contracts
  • [bio] for biological systems
  • [aut] for the automotive industry
  • [cld] for cloud computing


  • [con] REMU (2013-2017) [http://remu.grammaticalframework.org]
    Gerardo Schneider (gerardo(a)cse.gu.se)
    Part of this project is concerned with the definition of front-end and a back-end for contract analysis. There is an intention of developing runtime monitors for contracts defined in the C-O formalism, though this has not started yet.
  • [con] DataBiN (2012-2016) [http://www.cse.chalmers.se/research/databin]
    Gerardo Schneider (gerardo(a)cse.gu.se)
    One part of this project is about privacy. One of the research directions is to define privacy policies for social networks. The current status is the definition formal privacy framework based on epistemic logic to write privacy policies. Future work in this part of the project is to define runtime monitors for checking at runtime that the privacy policies are respected.
  • [bio,cps] Monitoring Spatio-Temporal Properties (2014-2015)
    Ezio Bartocci (ezio.bartocci(a)tuwien.ac.at)
    Networked dynamical systems are increasingly used as models for a variety of processes ranging from robotic teams to collections of genetically engineered living cells. As the complexity of these systems increases, so does the range of emergent properties that they exhibit. We have recently defined a new logic called Spatio-Temporal Logic (SpaTeL) that is a unification of signal temporal logic (STL) and tree spatial superposition logic (TSSL). SpaTeL is capable of describing high-level spatial patterns that change over time, e.g. “Power consumption in the northwest quadrant of the city drops below 100 megawatts if the power consumption in the southwest quadrant remains above 200 megawatts for two hours.” We present a statistical model checking procedure that evaluates the probability with which a networked system satisfies a SpaTeL formula. We have also developed a synthesis procedure that determines system parameters maximizing the average degree of satisfaction, a continuous measure that quantifies how strongly a system execution satisfies a given formula. We have tested our algorithms on two systems: a biochemical reaction-diffusion system and a demand-side management system for a smart neighbourhood.
  • [med] Mining and monitoring signal patterns in medical signals (2014)
    Ezio Bartocci (ezio.bartocci(a)tuwien.ac.at)
    We have introduced a novel approach to automatically detect ineffective breathing efforts in patients in intensive care subject to assisted ventilation. The method is based on synthesising from data temporal logic formulae which are able to discriminate between normal and ineffective breaths. The learning procedure consists in first constructing statistical models of normal and abnormal breath signals, and then in looking for an optimally discriminating formula. The space of formula structures, and the space of parameters of each formula, are searched with an evolutionary algorithm and with a Bayesian optimisation scheme, respectively.
  • [cld] Cloud computing
    Boro Jakimovski (boro.jakimovski(a)finki.ukim.mk)
    Cloud computing is a very diverse field of software engineering covering every level of abstraction of the cloud (Infrastructure (IaaS), Platforms (PaaS) and Software (SaaS)) brings different problem sets for RV. IaaS’ main concerns, besides the virtualization of hardware resources, are reliability of cloud systems such as: Virtual machine lifecycle, network security, and properties of the storage system. PaaS is a very diverse field of platforms adopted to serve as a service. One of the most popular PaaS lately is container-based virtualization (e.g., Docker, OpenShift). This technology is developing rapidly, but isn’t prepared for production due to the uncertainty of its stability and security. SaaS concerns evolve from standard software problems, emphasized by software distributed nature of functioning. Usually SaaS uses technologies, like databases or key-value stores, which are not transactional based, due to the non-scalability of synchronization between vast number of servers hosting the platform. Application of RV in SaaS can be towards monitoring of properties based traces of distributed transactions of applications.
    Currently our focus is on large volume log management tools and trying to integrate RV capabilities into them. These log management tools are scalable and elastic and can provide handling of large log volumes from distributed and diverse sources. Monitoring IaaS logs for VM lifecycle is another field that we are currently working on.