Behavioral an real-time verification of a pipeline in the COSMA environment
This is an incremental case study on model checking for a specific pipeline system in the COSMA environment.
The paper tackled the verification of a three-stage pipeline with concurrent modules competing for a shared resource in the COSMA environment, using Concurrent State Machines (CSM) to specify components and applying model checking, reduction, counter-example analysis, and real-time property verification.
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.