https://www.um.edu.mt/library/oar/handle/123456789/63124 Thu, 16 Apr 2026 01:32:08 GMT 2026-04-16T01:32:08Z https://www.um.edu.mt/library/oar/handle/123456789/83645 Title: Runtime verification for API based software Abstract: The modern world is increasingly dependent on communication-centred and distributed software systems. Application Programming Interfaces (APIs) are what enable these systems to interact and share information with one another. The correctness of their interaction is of utmost importance since the consequences of failure can be quite severe. Behavioural types offer a promising approach to address this matter by enabling the description of correct interactions which systems are then verified against. This work investigates the design and implementation of a hybrid (static and dynamic) approach for the verification of these types. In particular, we address those scenarios with two communicating components where one is available prior-deployment and the other must be treated as a black box. We propose an approach in which the available component is statically checked whereas the black box component is verified dynamically at runtime (i.e., during execution) via a monitor. At the centre of our approach is a synthesis algorithm which generates monitor descriptions from a behavioural type. We show that these generated monitors are themselves correct, and that they only flag an erroneous action when the monitored component indeed commits one. This is crucial since the monitors can negatively affect the behaviour of the other components if they are not correct. To validate the implementability of this approach, we present a tool in Scala as a case study. We show that the executable code closely follows the theory, which suggests that the notion of correctness established in the theory carries over into the implementation. Furthermore, the proposed theory and implementability aspects of our approach are not limited to this technology but can be applied to those cases where static analysis of session types is possible and the dynamic verification of the interaction of a component is required. Description: M.SC.COMPUTER SCIENCE Wed, 01 Jan 2020 00:00:00 GMT https://www.um.edu.mt/library/oar/handle/123456789/83645 2020-01-01T00:00:00Z https://www.um.edu.mt/library/oar/handle/123456789/71908 Title: Behavioural APIs for Erlang processes Abstract: Behavioural Application Programming Interfaces (APIs) (12) consist of the amalgation of traditional APIs with formal behavioural information related to their usage. These newer versions of APIs are frequently being utilised in concurrent systems whereby communication between numerous processes is required. Message-passing is one of the main forms of communication mechanisms that was deemed fit to be utilised throughout this dissertation. This thesis studies the behaviour of processes in a network and identifies the gap between existent approaches to message-passing communication systems and their implementation using the features available in Erlang-based programming languages. The foundational framework utilized throughout this study is the Mailbox Calculus, proposed by the ‘Liguoro and Padovani (16) in their paper entitled ‘Mailbox Types for Unordered Interactions’. This message-passing system provided the added benefits of ensuring certain software guarantees, including deadlock freedom, fault tolerance and mailbox compliance. In the first part of this thesis, the syntax of the Mailbox Calculus is translated into an appropriate formal definition which is then implemented in Elixir; an Erlang-based functional programming language. Additionally, slight modifications and extensions to this syntax were carried out in accordance with existent Elixir features. The implementation part is comprised of a lexer and a parser specifically created for the target language MC2Elixir; which is an adaptation of the Mailbox Calculus. In the second part of this thesis an interpreter and launcher are constructed test and verify the correctness of the implemented artefact. Elixir is inherently a weakly-typed language (33); thus, trying to find Elixir constructs corresponding to those in the strongly-typed Mailbox Calculus, was one of the main challenges encountered throughout this dissertation. Nonetheless, the final proposed system MC2Elixir visibly encompasses the main features of the Mailbox Calculus. Description: B.SC.(HONS)COMP.SCI. Wed, 01 Jan 2020 00:00:00 GMT https://www.um.edu.mt/library/oar/handle/123456789/71908 2020-01-01T00:00:00Z https://www.um.edu.mt/library/oar/handle/123456789/71901 Title: Using machine learning to predict epileptic seizures from EEG data Abstract: With the recent progress in Machine Learning (ML) and Artificial Intelligence (AI), researchers aim to apply techniques for improving and automating certain facets of clinical practice. One of the more intriguing and compelling applications of modern computing in a healthcare context is the early detection and prediction of life threatening events. In the case of epilepsy, the prediction of seizure onsets would allow patients to appropriately prepare for such recurrent episodes of convulsion, which in turn improves their quality of life. Albeit seizures are preventable by specific medication and therapies, it is common for patients to suffer from intractable seizures, which is the result of drug-resistant epilepsy. The prediction of seizure onsets would allow patients some relief in knowing when to be prepared and when to avoid dangerous activities such as driving. This Bachelor’s dissertation presents a review of the performance of a set of supervised machine learning methods for the task of seizure prediction. The study involves using a dataset that includes non-invasive scalp Electroencephalography (EEG) signals, which are brain electrophysiological readings that did not involve surgery. Subsequent to data pre-processing, statistical and wavelet features from the signals were extracted, and the results obtained from K-Nearest Neighbour (KNN), Support Vector Machines (SVM), and an Ensemble Classifier are compared. Results are reported on the CHB-MIT dataset, which includes 192 seizure readings from 22 patients suffering from intractable seizures. The study shows that the three methods perform similar, although the Ensemble Classifier achieves a higher specificity, sensitivity and accuracy. Description: B.SC.(HONS)COMP.SCI. Wed, 01 Jan 2020 00:00:00 GMT https://www.um.edu.mt/library/oar/handle/123456789/71901 2020-01-01T00:00:00Z https://www.um.edu.mt/library/oar/handle/123456789/71899 Title: Learning models using similarity based and one vs previous paradigms Abstract: Traditionally, when building machine learning models for multi-class classifi cation, it is common practice to build a model consisting of an ensemble of binary classifiers using some learning paradigm which dictates how the binary classifi ers work together to discriminate between the individual classes. As new data comes in and the model needs updating, these models would often need to be retrained from scratch. This work considers three new learning paradigms which provide a way for the trained models to update without the need of retraining the entire system from scratch. Through training class by class, we utilize previous classifi ers for previous classes to build more efficient classifi ers for future classes, which gives the paradigms applications in Lifelong Machine Learning, by avoiding training against the examples of classes which would provide no bene t to our new classifi er's classification performance. The goal is to create models which are reusable and take less time to train while retaining classifi cation performance. Results show that the new paradigms are promising in different scenarios with regards to their goal. Description: B.SC.(HONS)COMP.SCI. Wed, 01 Jan 2020 00:00:00 GMT https://www.um.edu.mt/library/oar/handle/123456789/71899 2020-01-01T00:00:00Z