Below is a list of existing industrial case studies. If the case study 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
- [fin] Credit card and transaction processor (2007-2008)
Christian Colombo (christian.colombo(a)um.edu.mt)
An international high-volume transaction-processing company with a software development house in Malta (due to the terms of our non-disclosure agreement, the name of the company cannot be disclosed) has allowed the University of Malta to apply runtime verification techniques on its system. The kind of properties which have been checked involved ensuring no credit card numbers leak to the logs, transactions follow the expected life cycle, and that the number of retries of a transaction are as limited to three.
Unfortunately, to the best of our knowledge, runtime verification has not been taken up in newer versions of their product.
- [fin] Ixaris Systems Malta Ltd (2008-present)
Christian Colombo (christian.colombo(a)um.edu.mt)
Ixaris Systems Malta Ltd has been a strong supporter of runtime verification. A substantial case study has been carried out from 2008 till 2010 focusing on specifying and monitoring of correctness properties in an offline fashion. The reason for opting for offline monitoring was that the company felt that it was not ready to trust runtime monitoring code to run alongside its live system. Thus, a database dump was collected at regular intervals and this was checked according to the specified correctness properties. Similarly to the above case these involved checking the life cycle of transactions, that daily/weekly/monthly limits are observed, inactive accounts are disabled, etc.
Since then there have been further applications of runtime verification at Ixaris. Interestingly, the application is not strictly runtime verification in the usual sense of the word: A common issue with web portals is to ensure that the user interface is suitably organised and that users are navigating and accessing the features with ease. For this reasons, user interface logs – including clicks, data entry, etc – were fed into a runtime monitor to gather statistics regarding the time and number of steps needed by the user to complete certain tasks.
The latest development in recent months involved the possibility of incorporating runtime monitoring as a service in a service-oriented transaction processing architecture. This would enable the monitor to be non-intrusive but at the same time running within the live system, possibly detecting problems soon after they occur.
- [aut] Assertion-based Hardware Monitors for Automotive Systems (2014-2017)
Ezio Bartocci (ezio.bartocci(a)gmail.com)
HARMONIA is a project funded by the Austrian FFG, with TU Wien, Austrian Institute of Technology and Infineon as main PIs. The aim of HARMONIA 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 and performance properties of such systems. Observers embedded on FPGA hardware will be generated from assertions, and used for monitoring automotive designs emulated on hardware.
- [dcs] Real-time distributed control systems
Leonardo Mariani (mariani(a)disco.unimib.it)
The aim of this project was to apply analysis techniques on the ABB FASA system — a real-time software framework for distributed control systems developed at ABB Corporate Research. The objective of the control software is to protect equipment from unexpected and dangerous situations. The controller can determine if the system is healthy from measurements received from sensors. If something wrong is detected, the controller activates proper protection functions that can prevent any serious damage or side effect for the system.
The project applied the RADAR automated debugging solution to faults injected in the ABB FASA system. RADAR can analyse regression problems and automatically identify the chain of erroneous events that lead to a failure in a C/C++ program. To this end, it uses a combination of static analysis, to determine the portion of the program affected by a change, specification mining, to generate finite state machines and program invariants that capture the behaviour of the program, and runtime verification, to verify the mined specifications against the behaviour of the program and determine the suspicious events.
Papers about RADAR:
Fabrizio Pastore, Leonardo Mariani, Alberto Goffi, Manuel Oriol, Michael Wahler: Dynamic Analysis of Upgrades in C/C++ Software. ISSRE 2012: 91-100
Fabrizio Pastore, Leonardo Mariani, Alberto Goffi: RADAR: a tool for debugging regression problems in C/C++ software. ICSE Tool Demo 2013: 1335-1338