# 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.

## Key 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.

---
Source: https://tomesphere.com/paper/1703.05523