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-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
Study-unit Registration Forms 2017/8

Register

For Undergraduate (Day) and Postgraduate students.

 

Faculty of ICT Timetables

Timetables

ICT Timetables are available from Here.

Communicating Process Architectures 2017

CPA2017S

Taking place between the 20th August 2017 and 23rd of August 2017. More details from HERE.

 
 
Last Updated: 18 September 2017

Log In back to UoM Homepage
University of Malta
L-Università ta' Malta