Please use this identifier to cite or link to this item:
https://www.um.edu.mt/library/oar/handle/123456789/86108
Title: | Pushing runtime verification to the limit : may process semantics be with us |
Authors: | Della Monica, Dario Francalanza, Adrian |
Keywords: | Computer software -- Verification Computer logic Computer software -- Development Software engineering Semantics |
Issue Date: | 2019 |
Publisher: | CEUR Workshop Proceedings |
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. |
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. |
URI: | https://www.um.edu.mt/library/oar/handle/123456789/86108 |
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.