University of Malta
 

Technical Reports
UOM Main Page
 
 
 
Apply - Admissions 2016
Newspoint
Campus Map button
Facebook
Twitter

Technical Report Series


The Department of Computer Science of the University of Malta maintains this Technical Report Series, in which current research carried out by staff members and students can be published.

If you require any further information, please contact reports@cs.um.edu.mt.

The LaTeX class file for the technical report series, and an example dummy report can be downloaded from here.

Report

CS-2019-01
Title Porthos: Macroprogramming Blockchain Systems
Authors Adrian Mizzi, Joshua Ellul, and Gordon J. Pace
Abstract

The rise of blockchain technology has paved the way for an increasing number of blockchain systems, each having different characteristics. The need for distributed applications that span across multiple blockchain systems is increasing and in particular, there is a need for the ability to write a single-description smart contract which can be compiled to span across multiple blockchain systems.

In this paper we present Porthos, a macroprogramming framework and domain specific language for writing commitment-based smart contracts that span multiple blockchain systems. The language allows programmers to write smart contracts at a higher level of abstraction by composing together contract blocks, without the need to specify how logic should be split across different blockchain instances. A runtime framework, including both on-chain and off-chain functionality, harmonises the features of different blockchain systems as well as enables communication across the smart contracts. A proof of concept, built on the Ethereum and Hyperledger Fabric blockchain systems and extendible to other systems, illustrates the technique and framework. We also show how the Porthos language is expressive enough to define a variety of applications.

Downloads PDF

Report

CS-2018-01
Title

Securing Calls to Ethereum Smart Contracts with Static and Dynamic Analysis

Authors

Shaun Azzopardi, Christian Colombo, and Gordon J Pace

Abstract

Blockchains decentralise computation and storage, reducing the possibility that vulnerabilities in one node can affect a whole network. Ethereum is a popular implementation of these that acts as a distributed operating system for programs called smart contracts. Issues with these smart contracts have led to millions of tokens with real-world value being lost, motivating the need for formal analysis. One delicate issue is that once a smart contract is deployed to an address on the blockchain, its behaviour can be dependent on other smart contracts on the blockchain space, not just its own code or state. This creates issues for verification of a smart contract, given sound analysis requires modeling function calls to other smart contracts.

In this paper we consider the case of developed smart contracts which can use the functionality of other smart contracts possibly not developed by the same person. We propose the use of assume-guarantee reasoning that allows us to provide static guarantees about call sites in a user’s smart contract given assumptions provided by the service provider, assumptions which can then be discharged at runtime. We use symbolic automata as our specification language, defining a strictness relation between them, and a quotient or residual operation that allows us to prune proven parts away from a specification.

Downloads PDF

Report

CS-2017-02
Title A Timed Contract-Calculus
Authors Maria Emilia Cambronero, Luis Llana, and Gordon J. Pace
Abstract Over these past years, formal reasoning about contracts between parties participating in a transaction has been increasingly explored in the literature. There has been a shift of view from that viewing contracts simply as properties to be satisfied by the parties to contracts as first class syntactic objects which can be reasoned about independently of the parties' behaviour. In this paper, we present a contract calculus to reason about contracts abstracting the parties' behaviour in a simulation relation.  We study the contracts evolution in time by associating time constraints with deontic clauses, which allows to associate time limit with permissions, obligations and prohibitions. Then, we show how the calculus can be used to support the runtime monitoring of contracts and apply it to a plane boarding system case study.     
Downloads PDF

Report

CS-2017-01
Title

Control-Flow Residual Analysis for Symbolic Automata

Authors

Shaun Azzopardi, Christian Colombo, and Gordon J Pace

Abstract

Where full static analysis of systems fails to scale up due to system size, dynamic monitoring has been increasingly used to ensure system correctness. The downside is, however, runtime overheads which are induced by the additional monitoring code instrumented. To address this issue, various approaches have been proposed in the literature to use static analysis in order to reduce monitoring overhead. In this paper we generalise existing work which uses control-flow static analysis to optimise properties specified as automata, and prove how similar analysis can be applied to more expressive symbolic automata - enabling reduction of monitoring instrumentation in the system, and also monitoring logic. We also present empirical evidence of the effectiveness of this approach through an analysis of the effect of monitoring overheads in a financial transaction system.
Downloads PDF

Report

CS-2015-01
Title A Framework for the Generation of Computer System Diagnostics in Natural Language using Finite State Methods
Authors Rachel Farrell, Gordon J. Pace and Michael Rosner
Abstract The need for understanding what has lead to a failure in a computer system is crucial for addressing problems with such systems. In this report we present a meta-NLG system that can be con figured to generate natural explanations from error trace data originating in an external computational system. Distinguishing features are the generic nature of the system, and the underlying technology which is fi nite-state. Results of a two-pronged evaluation dealing with naturalness and ease of use are described.
Downloads PDFBiBTeX

Report

CS-2014-02
Title Computer Science Annual Workshop 2014
Authors Computer Science Department
Downloads PDFBiBTeX

Report

CS-2014-01
Title Extending Contract Automata with Reparations
Authors Shaun Azzopardi, Gordon J. Pace and Fernando Schapachnik
Abstract Although contract reparations have been extensively studied in the context of deontic logics, there is not much literature using reparations in automata-based deontic approaches. Contract automata are a recent approach to modelling the notion of contract- based interaction between diff erent parties using synchronous com- position. However, it lacks the notion of reparations for contract violations. In this article we look into diff erent ways reparation can be added to an automaton-based contract approach, extended contract automata with three forms of such clauses: (i) catch-all reparations for violation; (ii) reparations for specific violations; and (iii) hierar- chical contracts for local reparation reasoning.
Downloads PDFBiBTeX

Report

CS-2013-02
Title Computer Science Annual Workshop 2013
Authors Computer Science Department
Downloads PDFBiBTeX

Report

CS-2013-01
Title Synthesising Correct Concurrent Runtime Monitors in Erlang
Authors Adrian Francalanza and Aldrin Seychell
Abstract In this paper, we study the correctness of automated synthesis for concurrent monitors. We adapt sHML, a subset of the Hennessy-Milner logic with recursion, to specify safety properties of Erlang programs. We formalise an automated translation from sHML formulas to Erlang monitors that analyse systems at runtime and raise a flag whenever a violation of the formula is detected, ans use this translation to build a prototype runtime verification tool. Monitor correctness for concurrent setting is then formalised, together with a technique that allows us to prove monitor correctness in stages, and use this technique to prove the correctness of our automated monitor synthesis and tool.
Downloads PDFBiBTeX

Report

CS-2012-03
Title Computer Science Annual Workshop 2012
Authors Computer Science Department
Downloads PDFBiBTeX

Report

CS-2012-02
Title Compositional Reasoning for Explicit Resource Management in Channel-Based Concurrency
Authors Adrian Francalanza, Edsko de Vries, and Matthew Hennessy
Abstract We define a pi-calculus variant with a costed semantics where channels are treated as resources that must  explicitly be allocated before they are used and can be deallocated when no longer required. We use a substructural type system tracking permission transfer to construct compositional proof techniques for comparing behaviour and resource usage efficiency of concurrent processes.
Downloads PDFBiBTeX

Report

CS-2012-01
Title Separating Compensation Concerns and Programming them with Compensating Automata
Authors Christian Colombo and Gordon J. Pace
Abstract

Compensations have been used for decades in areas such as flow management systems, long-lived transactions and more recently in the service-oriented architecture. Since compensations enable the logical reversal of past actions, by their nature they cross-cut other programming concerns. Thus, intertwining compensations with the rest of the system not only makes programs less well-structured, but also limits the expressivity of compensations due to the tight coupling with the system's behaviour. 

To separate compensation concerns from the normal forward behaviour of the system, we propose a novel design paradigm in which compensations are programmed separately from the system, and incorporated within a compensation manager following relevant system events and manages compensations. If the system signals the need to be compensated, the manager triggers the execution of compensations on behalf of the system and subsequently returns control to the system. We show that this approach can be used to program a sophisticated real-life case study which existing compensation approaches have difficulty in handling. 

Downloads PDFBiBTeX

Report

CS-2011-02
Title An Event-Driven Language for Cartographic Modelling of Knowledge in Software Development Organisations
Authors Mark Micallef and Christian Colombo
Abstract With software engineering now being considered a fully-fledged knowledge industry in which the most valuable asset to an organisation is the knowledge held by its employees, high staff turnover rates are becoming increasingly worrying.  If software engineering organisations are to maintain their competitive edge, they need to ensure that their intellectual capital continues to grow and is not lost as people move in and out of their employ.
In this paper, the authors present work involving the formalisation of a language that enables organisations to create and analyse maps of their organisational knowledge.  In a more elaborate version of the traditional yellow-pages approach utilised in the cartographic school of thought, the proposed language models various relationships between knowledge assets, uses an event-driven mechanism to determine who knows what within the organisation, and finally provides metrics for detecting three types of risk related to knowledge management in modern software engineering.  A three month evaluation of the language is also outlined and results discussed.
Downloads PDF, BiBTeX
Report CS-2011-01
Title A Compensating Transaction Example in Twelve Notations
Authors Christian Colombo and Gordon J. Pace
Abstract The scenario of business computer systems changed with the advent of cross-entity computer interactions: computer systems no longer had the limited role of storing and processing data, but became themselves the players which actuated real-life actions. These advancements rendered the traditional transaction mechanism insufficient to deal with these new complexities of longer multi-party transactions. The concept of compensations has long been suggested as a solution, providing the possibility of executing "counter"-actions which semantically undo previously completed actions in case a transaction fails. There are numerous design options related to compensations particularly when deciding the strategy of ordering compensating actions. Along the years, various models which include compensations have emerged, each tackling in its own way these options. In this work, we review a number of notations which handle compensations by going through their syntax and semantics --- highlighting the distinguishing features --- and encoding a typical compensating transaction example in terms of each of these notations.
Downloads PDF, BiBTeX
Report CS-2009-02
Title Embedded Languages for Business Process Modelling, Transformation and Quality Assurance in Business-Driven Development
Authors Luana Micallef and Gordon J. Pace
Abstract
In Business-Driven Development (BDD), process models are produced by business analysts. To ensure that the defined requirements are satisfied, the IT solution must ideally be derived directly from the specifications through a process of model refinement. However, if the original models contain errors or lack some technical detail, an incorrect implementation would be inferred and the entire BDD life-cycle would have to be revised. In this report, we investigate the use of embedded language techniques to enable more abstract model descriptions and enable quality assurance and transformation of models. We have embedded such a domain-specific language in the functional programming language Haskell and show how it enables: (i) the rapid development of models in a concise and abstract manner, focusing on the specifications rather than the implementation and ensuring that all the required details to generate the executable code are specified; (ii) quality assurance of the models through the use of Haskell's type checker, at construction-time and through soundness analysis; (iii) transformation, analysis and interpretation of the models; and (iv) definition of composite model transformations, including the use of quality assurance.
Downloads
PDF, BiBTeX
Report CS-2009-01
Title Resource-Bounded Runtime Verification of Java Programs with Real-Time Properties
Authors Christian Colombo, Gordon J. Pace and Gerardo Schneider
Abstract Given the intractability of exhaustively verifying software, the use of runtime verification, to verify single execution paths at runtime, is becoming increasingly popular. Undoubtedly, the overhead introduced by runtime verification is a concern for system developers planning to introduce this technique in their work. By using Lustre to write security-critical properties, we exploit the language's guarantees on bounded resources. We translate these properties into the existing monitoring framework Larva, making monitoring of programs both easily applicable to Java programs and at the same time guarantee to use bounded-resources. We use a subset of Quantified Discrete-time Duration Calculus (QDDC) as an alternative specification notation for real-time properties because it is translatable into Lustre. Thus, QDDC also enjoys the same guarantees given when using Lustre.
Downloads PDF, BiBTeX
Report CSAI-2008-01
Title Multi-Stage Languages in Hardware Design
Authors Gordon J. Pace and Christian Tabone
Abstract As circuits increase in size and complexity, hardware description techniques have been trying to adopt features already wellestablished in software languages. In this paper, we investigate how different hardware description languages implement levels of abstraction over the hardware designs, and we examine how improvements have lead to features like parameterised circuits and generic descriptions, that enable users to efficiently model and reason about large regular-shaped structures and connection patterns. Nonetheless, the ability to include non-functional properties of circuits in the same description is still an open issue. Lately, proposed solutions are looking into meta-functional languages and multi-staging techniques. We examine how hardware description languages can benefit from the capabilities of meta-functional languages, which are able to reason about, and transform the circuit generators as data objects, thus providing a means to access both the functional and non-functional aspects of the generated circuits.
Downloads PDF, BiBTeX
Report CSAI-2007-01
Title Proceedings of CSAW'07
Authors Claudia Borg, Sandro Spina and Charlie Abela
Abstract This report contains the proceedings of the fifth Computer Science Annual Workshop (CSAW’07) - the research workshop held by the Departments of Computer Science and Artificial Intelligence of the University of Malta.
Downloads
PDF, BiBTeX
Report CSAI-2006-01
Title Proceedings of CSAW'06
Authors John Abela, Angelo Dalli and Kristian Guillaumier
Abstract This report contains the proceedings of the fourth Computer Science Annual Workshop (CSAW’06) - the research workshop held by the Departments of Computer Science and Artificial Intelligence of the University of Malta.
Downloads PDF, BiBTeX
Report CSAI-2005-02
Title Proceedings of CSAW'05
Authors Ernest Cachia and Mark Micallef
Abstract This report contains the proceedings of the third Computer Science Annual Workshop (CSAW’05) - the research workshop held by the Departments of Computer Science and Artificial Intelligence of the University of Malta.
Downloads PDF, BiBTeX
Report CSAI-2005-01
Title Automatic Document Clustering using Topic Analysis
Authors Robert Muscat
Abstract In this work we look at the automated organisation of documents in a document base into clusters and cluster hierarchies. We apply topic segmentation to detect topics within documents and using term relationships attempt to build hierarchies which represent a "real world" topic hierarchy. Finally, we assign documents to each of these topics using a standard clustering technique. We also propose two evaluation methods for document clustering systems. The first is an adaptation of tree measure algorithms to document hierarchies. The use of this method will require a pre-defined tree which has been agreed upon as a suitable benchmark. The second is independent of any benchmark trees and presents the evaluator with a number of measures which al low him to assess the properties of the tree.
Downloads PDF, BiBTeX
Report CSAI-2004-02
Title Proceedings of CSAW'04
Authors Gordon J. Pace and Joseph Cordina
Abstract This report contains the proceedings of the second Computer Science Annual Workshop (CSAW’04) - the research workshop held by the Departments of Computer Science and Artificial Intelligence of the University of Malta.
Downloads
PDF, BiBTeX
Report
CSAI-2004-01
Title
Support Vector Machines with Profile-Based Kernels for Remote Protein Homology Detection
Authors
Steven Busuttil, John Abela and Gordon J. Pace
Abstract
Two new techniques for remote protein homology detection particulary suited for sparse data are introduced. These methods are based on position specific scoring matrices or profiles and use a support vector machine (SVM) for discrimination. The performance on standard benchmarks outperforms previous non-discriminative techniques and is comparable to that of other SVM-based methods while giving distinct advantages.
Downloads
PDF, BiBTeX
Report
CSAI-2003-02
Title
Proceedings of CSAW'03
Authors
Gordon J. Pace and Joseph Cordina
Abstract
This report contains the proceedings of the first Computer Science Annual Workshop (CSAW’03) - the research workshop held by the Departments of Computer Science and Artificial Intelligence of the University of Malta.
Downloads
PDF, BiBTeX
Report
CSAI-2003-01
Title
A New Breadth-First Search Algorithm for Deciding SPDI Reachability
Authors
Gordon J. Pace
Abstract
Polygonal hybrid systems are a subclass of planar hybrid automata which can be represented by piecewise constant differential inclusions (SPDIs). Using an important object of SPDIs’ phase portrait, the invariance kernels, which can be computed non-iteratively, we present a breadth-first search algorithm for solving the reachability problem for SPDIs. Invariance kernels play an important role in the termination of the algorithm.
Downloads
PDF, BiBTeX 
Calendar
Notices
FICT Exhibition 2019 Form

Please click here to download the FICT Exhibition form for 2019. 

THE FICT Exhibition 2019 will be held on Thursday 11th and Friday 12th July 2019.

Academic Advisors 2018/9

AA1

Academic Advisors for ICT 1st year students (Intake 2018/9), NOW available

Faculty of ICT Timetables

Timetables

ICT Timetables are available from Here.

Health and Safety Regulations for Labs Form

The Faculty of ICT Health and Safety Regulations for Laboratories form can be found here

 HealthAndSafety

Digital Opportunity Traineeship

 

Are you a company working with cybersecurity, big data, quantum technology, machine learning or digital marketing? Offer a Digital Opportunity Traineeship

Test Island Conference

Test Island Conference (https://www.testisland.com/), Malta's first conference on Software Testing, jam-packed with high-profile international speakers, will be held on 30th August 2019. Dr Mark Micallef from the Faculty of ICT will be delivering the keynote speech. Click here for more information. 

 
 
Last Updated: 7 March 2019

Log In back to UoM Homepage