Message-Passing Based Communication via Asynchronous Execution (Shunts)
Nayef H. Alshammari · 2025
In this paper, a Parallel Runtime Verification Framework (PRVF) is presented. It can handle parallel systems using message-passing based communication via asynchronous execution mode. The proposed model can check systems behaviour at runtime in order to either guarantee satisfaction or detect violation of correctness properties. Parallel systems have correctness properties different from correctness properties of sequential systems. For instance, as a correctness property of parallel systems, absence of deadlock has to be guaranteed and mutual exclusion mechanism has to be applied in case a resource is shared between more than one system and the parallelism form is true concurrency. Therefore, sequential runtime verification framework cannot handle systems that run in parallel due to a structural limitation of this kind of framework as they are built to handle a single system at a time, whereas for parallel systems a framework has to handle many systems at a time. Several Challenges of parallel programs correctness are addressed at hardware and software levels. A theoretical comparison among verification techniques including theorem proving, model checking, testing, and runtime verification is highlighted. The applied technique is based on Interval Temporal Logic (ITL). A comprehensive description of the main components of PRVF and their functions is given.