Please use this identifier to cite or link to this item:
https://www.um.edu.mt/library/oar/handle/123456789/113320
Full metadata record
DC Field | Value | Language |
---|---|---|
dc.date.accessioned | 2023-09-26T08:58:54Z | - |
dc.date.available | 2023-09-26T08:58:54Z | - |
dc.date.issued | 2023 | - |
dc.identifier.citation | Sciberras, E. (2023). Runtime verification program side‐effects in OCaml (Bachelor’s dissertation). | en_GB |
dc.identifier.uri | https://www.um.edu.mt/library/oar/handle/123456789/113320 | - |
dc.description | B.Sc. (Hons)(Melit.) | en_GB |
dc.description.abstract | The paper aims to ensure the correctness of functional programs, written in OCaml. Despite being known for its functional programming features, OCaml provides support for imperative programming through the use of references, which are mutable variables enabling the sharing of states. However, their use in functional programming can introduce sofware bugs typically associated with non‐deterministic behaviour. The paper addresses these challenges through runtime verification, a technique that monitors OCaml program execution and checks for adherence to safety properties. This technique involves instrumenting the program to generate a trace that captures information about the events occurring during the OCaml program execution, including reads, writes, and references initalisations. The synthesised trace will be passed to monitors to enable runtime verificaton and analysis of critical events that capture program behaviour. The monitor will leverage as a formal method to detect and fag violations in real‐tme, ensuring correctness and robustness of the System under Scrutiny (SuS). To formally specify the properties, this project aims to verify using the sub‐logic of safety fragment of Hennessy‐Milner logic with recursion (sHML) [1], which is a syntactic subset of Hennessy‐Milner Logic with recursion (HML) [2]. This logic is used to specify and implement safety properties for our Runtime Verifcaton (RV) tool detectEr. Using sHML to express the properties to be checked, the project aims to generate synthesised properties that capture the essential program behaviour aspects [3], ensuring correctness. The project uses a monitoring algorithm to check the synthesised propertes against the program’s trace during executon. In order to ensure correctness, lists of events must undergo formal verifcaton. The monitoring algorithm then applies runtme analysis techniques to detect potental violatons of system propertes. Based on the analysis results, boolean fags are generated to indicate the presence or absence of a violaton. This simplifes the process of locatng and reportng any violatons that may arise in the OCaml program, thereby ensuring program correctness, robustness, and overall quality of the running SuS. | en_GB |
dc.language.iso | en | en_GB |
dc.rights | info:eu-repo/semantics/restrictedAccess | en_GB |
dc.subject | OCaml (Computer program language) | en_GB |
dc.subject | Functional programming (Computer science) | en_GB |
dc.subject | Computer software -- Verification | en_GB |
dc.subject | Computer logic | en_GB |
dc.title | Runtime verification program side‐effects in OCaml | en_GB |
dc.type | bachelorThesis | en_GB |
dc.rights.holder | The copyright of this work belongs to the author(s)/publisher. The rights of this work are as defined by the appropriate Copyright Legislation or as modified by any successive legislation. Users may access this work and can make use of the information contained in accordance with the Copyright Legislation provided that the author must be properly acknowledged. Further distribution or reproduction in any format is prohibited without the prior permission of the copyright holder. | en_GB |
dc.publisher.institution | University of Malta | en_GB |
dc.publisher.department | Faculty of Information and Communication Technology. Department of Computer Science | en_GB |
dc.description.reviewed | N/A | en_GB |
dc.contributor.creator | Sciberras, Emma (2023) | - |
Appears in Collections: | Dissertations - FacICT - 2023 Dissertations - FacICTCS - 2023 |
Files in This Item:
File | Description | Size | Format | |
---|---|---|---|---|
2308ICTICT390705072407_1.PDF Restricted Access | 1.44 MB | Adobe PDF | View/Open Request a copy |
Items in OAR@UM are protected by copyright, with all rights reserved, unless otherwise indicated.