Behavioral an real-time verification of a pipeline in the COSMA environment

Jerzy Mieścicki, Wiktor B. Daszczuk

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.

Full Text:

PDF


DOI: http://dx.doi.org/10.17951/ai.2006.4.1.254-265
Date of publication: 2006-01-01 00:00:00
Date of submission: 2016-04-27 10:15:09


Statistics


Total abstract view - 422
Downloads (from 2020-06-17) - PDF - 0

Indicators



Refbacks

  • There are currently no refbacks.


Copyright (c) 2015 Annales UMCS Sectio AI Informatica

Creative Commons License
This work is licensed under a Creative Commons Attribution 4.0 International License.