COSMA 环境中流水线的行为与实时验证
软件工程
2017-03-17 v1
摘要
本文分析的案例研究展示了 COSMA 环境中模型检验的实例。该系统本身是一个三级流水线，由相互并发且竞争共享资源的模块组成。系统组件以并发状态机（CSM）进行规约。本文展示了行为属性验证、模型归约技术、反例分析以及实时属性检验。
引用
@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}
}
备注
12 pages, 7 figures