Content area

Abstract

Translate

Multiparty session typing (MPST) is a formal method to make concurrent programming simpler. The idea is to use type checking to automatically prove safety (protocol compliance) and liveness (communication deadlock freedom) of implementations relative to specifications. Discourje is an existing run-time verification library for communication protocols in Clojure, based on dynamic MPST. The original version of Discourje can detect only safety violations. In this paper, we present an extension of Discourje to detect also liveness violations.

Details

1009240
Subject
Concurrent processing;
Program verification (computers);
Formal method;
Run time (computers)
Identifier / keyword
Programming Languages
URL
http://arxiv.org/abs/2407.00540
Title
Discourje: Run-Time Verification of Communication Protocols in Clojure -- Live at Last (Technical Report)
Author
Sung-Shik Jongmans
Publication title
arXiv.org; Ithaca
Publication year
2024
Publication date
Jun 29, 2024
Section
Computer Science
Publisher
Cornell University Library, arXiv.org
Source
arXiv.org
Place of publication
Ithaca
Country of publication
United States
University/institution
Cornell University Library arXiv.org
Publication subject
Biology, Statistics, Physics, Mathematics, Engineering--Electrical Engineering, Computers--Computer Engineering, Business And Economics--Banking And Finance
e-ISSN
2331-8422
Source type
Working Paper
Language of publication
English
Document type
Working Paper
Publication history
 
 
Online publication date
2024-07-02
Milestone dates
2024-06-29 (Submission v1)
Publication history
 
 
   First posting date
02 Jul 2024
ProQuest document ID
3074861889
Document URL
https://www.proquest.com/working-papers/discourje-run-time-verification-communication/docview/3074861889/se-2?accountid=208611
Full text outside of ProQuest
http://arxiv.org/abs/2407.00540
Copyright
© 2024. This work is published under http://creativecommons.org/licenses/by/4.0/ (the “License”). Notwithstanding the ProQuest Terms and Conditions, you may use this content in accordance with the terms of the License.
Last updated
2024-07-08
Database
ProQuest One Academic