Please use this identifier to cite or link to this item:
https://www.um.edu.mt/library/oar/handle/123456789/86108
Full metadata record
DC Field | Value | Language |
---|---|---|
dc.contributor.author | Della Monica, Dario | - |
dc.contributor.author | Francalanza, Adrian | - |
dc.date.accessioned | 2021-12-28T06:33:45Z | - |
dc.date.available | 2021-12-28T06:33:45Z | - |
dc.date.issued | 2019 | - |
dc.identifier.citation | Della Monica, D., & Francalanza, A. (2019). Pushing runtime verification to the limit : may process semantics be with us. 1st Workshop on Artificial Intelligence and Formal Verification, Logics, Automata and Synthesis (OVERLAY), Rende. 47-52. | en_GB |
dc.identifier.uri | https://www.um.edu.mt/library/oar/handle/123456789/86108 | - |
dc.description.abstract | We propose a combined approach that permits automated formal verification to be spread across the pre- and post-deployment phases of a system development, with the aim of calibrating the management of the verification burden. Our approach combines standard model checking methods with runtime verification, a relatively novel formal technique that verifies a system during its execution. We carry out our study in terms of the Hennessy-Milner Logic, a branching-time logic for specifying reactive system correctness. Whereas we will be mainly concerned with limiting the model checking verification burden, runtime verification has been shown to handle a strict subset of the expressible properties in our logic of study, posing constraints on what can be shifted to the post-deployment phase. We present a solution, based on modal transition systems and modal refinement, for the fragment of the Hennessy-Milner Logic devoid of recursion, i.e., without least and greatest fixpoint operators. | en_GB |
dc.description.sponsorship | This work is partially supported by the Italian INdAM-GNCS project Metodi formali per tecniche di verifica combinata, the Icelandic Research Fund project TheoFoMon: Theoretical Foundations for Monitorability (No.163406-051), and the project BehAPI, funded by the EU H2020 RISE programme under the Marie Skłodowska-Curie grant agreement (No.778233). | en_GB |
dc.language.iso | en | en_GB |
dc.publisher | CEUR Workshop Proceedings | en_GB |
dc.rights | info:eu-repo/semantics/openAccess | en_GB |
dc.subject | Computer software -- Verification | en_GB |
dc.subject | Computer logic | en_GB |
dc.subject | Computer software -- Development | en_GB |
dc.subject | Software engineering | en_GB |
dc.subject | Semantics | en_GB |
dc.title | Pushing runtime verification to the limit : may process semantics be with us | en_GB |
dc.type | conferenceObject | 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.bibliographicCitation.conferencename | 1st Workshop on Artificial Intelligence and Formal Verification, Logics, Automata and Synthesis (OVERLAY) | en_GB |
dc.bibliographicCitation.conferenceplace | Rende, Italy, 19-20/11/2019 | en_GB |
dc.description.reviewed | peer-reviewed | en_GB |
Appears in Collections: | Scholarly Works - FacICTCS |
Files in This Item:
File | Description | Size | Format | |
---|---|---|---|---|
Pushing Runtime Verification to the Limit.pdf | 698.36 kB | Adobe PDF | View/Open |
Items in OAR@UM are protected by copyright, with all rights reserved, unless otherwise indicated.