Model Checking in The COSMA Environment as a Support for The Design of Pipelined Processing
This addresses verification challenges for designers of pipelined processing systems, but appears incremental as it applies existing methods to a specific case study.
The paper tackled the problem of verifying a three-stage pipeline with concurrent modules competing for a shared resource, using Concurrent State Machines (CSM) and temporal model checking in the COSMA environment, resulting in a verified behavioral specification.
The case study analyzed in the report involves the behavioral specification and verification of a three-stage pipeline consisting of mutually concurrent modules which also compete for a shared resource. The system components are specified in terms of Concurrent State Machines (CSM) and the verification technique used is the temporal model checking in the COSMA environment.