Behavioral an real-time verification of a pipeline in the COSMA environment
Software Engineering
2017-03-17 v1
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.
Cite
@article{arxiv.1703.05523,
title = {Behavioral an real-time verification of a pipeline in the COSMA environment},
author = {Jerzy Mieścicki and Wiktor B. Daszczuk},
journal= {arXiv preprint arXiv:1703.05523},
year = {2017}
}
Comments
12 pages, 7 figures