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

Jerzy Mieścicki, Wiktor B. Daszczuk


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:


Data publikacji: 2006-01-01 00:00:00
Data złożenia artykułu: 2016-04-27 10:15:09


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



  • 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.