Behavioral an real-time verification of a pipeline in the COSMA environment

TL;DR

This paper demonstrates real-time verification of a concurrent pipeline system in the COSMA environment, including behavioral property checking, model reduction, and counter-example analysis.

Contribution

It introduces a method for verifying behavioral and real-time properties of concurrent systems using CSM in the COSMA environment.

Findings

Successful verification of behavioral properties

Effective model reduction techniques applied

Analysis of counter-examples provided insights

Abstract

The case study analyzed in the paper illustrates the example of model checking in the COSMA environment. The system itself is a three-stage pipeline consisting of mutually concurrent modules which also compete for a shared resource. System components are specified in terms of Concurrent State Machines (CSM) The paper shows verification of behavioral properties, model reduction technique, analysis of counter-example and checking of real time properties.