Model Checking in The COSMA Environment as a Support for The Design of Pipelined Processing
arXiv:1705.04728
Abstract
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.
15 pages, 11 figures, European Congress on Computational Methods in Applied Sciences and Engineering ECCOMAS 2004, Jyväskylä, Finland, 24-28 July 2004