vix.ing · top · new · best · stats · spec

Verifying Correctness of Shared Channels in a Cooperatively Scheduled Process-Oriented Language

2025/10/12 by Jan Bækgaard Pedersen, Pedersen, Jan, Kevin Chalmers +1
Business, Management and Accounting · Computer Science · #Advanced Software Engineering Methodologies #Business Process Modeling and Analysis #FOS: Computer and information sciences #Programming Languages (cs.PL) #Service-Oriented Architecture and Web Services

paper · pdf · doi:10.48550/arxiv.2510.11751

openalex publication_date 2025/10/12 · openalex created_date 2025/10/17 · openalex updated_date 2026/07/28

Abstract

Correct concurrent behaviour is important in understanding how components will act within certain conditions. In this work. we analyse the behaviour of shared communicating channels within a coorporatively scheduled runtime. We use the refinement checking and modelling tool FDR to develop both specifications of how such shared channels should behave and models of the implementations of these channels in the cooperatively scheduled language ProcessJ. Our results demonstrate that although we can certainly implement the correct behaviour of such channels, the outcome is dependant on having adequate resources available to execute all processes involved. We conclude that modelling the runtime environment of concurrent components is necessary to ensure components behave as specified in the real world.

Related