University of Malta
 

Page Contents
UOM Main Page
 
 
 
Newspoint
Facebook
Twitter

Runtime Verification

KD01GJP

 

The Invention 

Computer systems have become ever present in all the aspects of our lives with users demanding reliable, consistent and robust software.  Faults in such systems could lead to disgruntled consumers, data breaches as well as security breaches which could be financially costly.  Therefore, prior to being launched, software is tested against numerous user inputs and events. This allows developers to pick up on any errors and amend them before the product is implemented.  However, the system does not work in a vacuum and it is impossible to predict and simulate all the possible variations exhaustively especially in the case for large and complex systems. Testing code is also often the source of unexpected repercussions such as a system slowdown and memory overheads.

A complementary approach to support error handling is that of runtime verification.  This process automatically creates monitors which observe the system while in use in order to identify errors during runtime. Such errors can then be used to trigger appropriate response to rectify them. The system uses real-time user input, eliminating the need to create hypothetical inputs which is the main difficulty in testing, whilst also ensuring that runtime errors are addressed immediately.  

At the University of Malta we have developed the LARVA toolset, a runtime verification platform for runtime verification of critical systems, including Larva for Java programs, eLarva for Erlang systems and polyLarva, a language agnostic runtime verification system. These tools have been used on a number of industrial use cases.

 

Novelty

The technology allows for the runtime verification of software without needing too much processing power or memory access. It can also give an entire set of new possibilities to run any kind of rules to be tested over existing machines and software.  Monitoring can also be conducted without changing any code in the system being monitored.

LARVA use can be limited during the testing phase as well as utilised after the software has been deployed.  The input language used for LARVA has been kept simple in order to facilitate its use. Furthermore, LARVA allows for real-time clocks in the specification. These can be used to trigger events and measure the time elapsed between events. This can be very useful to describe numerous interesting properties such as that no more than 3 bad logins should be allowed with 10 minutes of each other.

 

Applications/ Industries

The technology has numerous applications, including:

  • Support in the financial and banking sector
  • Ensure fair play and adherence to contractual agreements relating to online betting
  • Cheat detecting in gaming 
  • Astronomy
  • Health management and diagnosis systems
  • Privacy policies for social networks
  • Mobile phone usage management for parental and organisational control

Development Status

The LARVA toolkit is available online

 

Intellectual Property Status

The software is protected by copyright. In Malta the Copyright Act applies.

 

Commercial Interest

We are looking for companies who may require specific contract languages for their area of operation.

 

Lead Originator and Relevant Publications

Prof. Gordon Pace and Dr. Christian Colombo

Semantics and Verification Research Group [Link]

polyLarva: Runtime Verification with Configurable System-Monitor Resource-Aware Boundaries, Christian Colombo, Adrian Francalanza, Ruth Mizzi and Gordon Pace,  Software Engineering and Formal Methods (SEFM), 2012.

LARVA - Safer Monitoring of Real-Time Java Programs, Christian Colombo, Gordon J. Pace and Gerardo Schneider, in Software Engineering and Formal Methods (SEFM), 20 

Fast-Forward Runtime Monitoring - An Industrial Case Study, Christian Colombo, and Gordon Pace, in the Proceedings of Runtime Verification (RV), 2012.

Safer Asynchronous Runtime Monitoring Using Compensations, Christian Colombo, Gordon Pace and Patrick Abela, in Formal Methods in System Design, 41(3): 269-294, 2012. 

Combining Testing and Runtime Verification Techniques, Kevin Falzon and Gordon Pace, in the Proceedings of 8th International Workshop on Model-based Methodologies for Pervasive and Embedded Software (MOMPES), 2012.

Organising LTL Monitors over Distributed Systems with a Global Clock, Christian Colombo and Ylies Falcone, in the Proceedings of Runtime Verification (RV), 2014.

Distributed System Contract Monitoring, Adrian Francalanza, Andrew Gauci, and Gordon Pace, in Journal of Logic and Algebraic Programming (JLAP), 2013.

A Specification Language for Static and Runtime Verification of Data and Control Properties, Jesus Mauricio Chimento, Wolfgang Ahrendt, Gordon Pace, and Gerardo Schneider, in the Proceedings of the 20th International Symposium on Formal Methods (FM 2015), 2015 

Verifying data- and control-oriented properties combining static and runtime verification: theory and tools, Wolfgang Ahrendt, Jesus Mauricio Chimento, Gordon J. Pace and Gerardo Schneider, in Formal Methods in System Design, pg1-66 DOI: 10.1007/s10703-017-0274-y, April 2017.

An Automata-based Approach to Evolving Privacy Policies for Social Networks, Raul Pardo, Christian Colombo, Gordon J. Pace and Gerardo Schneider, in Proceedings of the Seventh Conference on Runtime Verification 2016 (RV'16), Madrid, Spain, LNCS, 2016.

A Model-Based Approach to Combining Static and Dynamic Verification Techniques, Shaun Azzopardi, Christian Colombo and Gordon J. Pace, in 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2016), LNCS, 2016.

Runtime Verification for Stream Processing Applications, Christian Colombo and Gordon J. Pace, in 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2016), in LNCS, 2016.

On the Runtime Enforcement of Evolving Privacy Policies in Online Social Networks, Gordon J. Pace, Raúl Pardo and Gerardo Schneider, in 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2016), to appear in LNCS, 2016.

StaRVOOrS - Episode II, Strengthen and Distribute the Force, with Wolfgang Ahrendt, Gordon J. Pace and Gerardo Schneider, in 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2016), to appear in LNCS, 2016.

Automatically Generating Runtime Monitors from Tests, Abigail Cauchi, Luke Chircop, Christian Colombo, Adrian Francalanza, Gordon J. Pace and Mark Micallef, in the proceedings of the 1st VORTEX Workshop on Runtime Verification, 2016.

A Controlled Natural Language For Tax Fraud Detection, Aaron Calafato, Christian Colombo and Gordon J. Pace, in the Workshop on Controlled Natural Languages 2016 (CNL'16), to be published in LNCS, 2016.

Using Gherkin to Extract Tests and Monitors for Safer Medical Device Interaction Design, Abigail Cauchi, Christian Colombo, Adrian Francalanza, Gordon J. Pace and Mark Micallef, in the Proceedings of the 8th ACM SIGCHI Symposium on Engineering Interactive Computing Systems, 2016.

Compliance Checking in the Open Payments Ecosystem, Shaun Azzopardi, Christian Colombo, Gordon J. Pace and Brian Vella, in the Proceedings of the 14th International Conference on Software Engineering and Formal Methods (SEFM 2016), 2016.

Device-Centric Monitoring for Mobile Device Management, Luke Chircop, Christian Colombo and Gordon J. Pace, in the Proceedings of the International Workshop on Formal Engineering approaches to Software Components and Architectures 2016 (FESCA 2016), 2016 [PDF]

Think Magazine - Trusting the Machine [Link]

Research Projects [Link]

ARVI COST launched in Malta [Link]


 

Download Summary [PDF]

 

Interested? Contact Nicola Camilleri or the Knowledge Transfer Office.  

Calendar
Notices
TAKEOFF Seed Fund Award- Applications Open!
TAKEOFF Seed Fund Award to support entrepreneurs and researchers
Launching Funding Fridays
Drop into Level 3, Dar Guzeppi Zahra every Friday for funding support. 

Funding Fridays is an initiative of the Knowledge Transfer Office and the Project Support Office offering the academics dedicated support services in relation to European and national research funds in order to increase application and success rate. 
Industry Placements Available!
Check out www.um.edu.mt/placements
Student with a Business Plan?

‘ERASMUS FOR YOUNG ENTREPRENEURS’ is the programme for you!

 
 
Last Updated: 4 May 2017

Log In back to UoM Homepage