ROSA Analyser：一种分析 ROSA 进程的自动化方法
软件工程
2012-07-12 v1
摘要
本文介绍了 ROSA Analyser 的首个版本，该工具旨在实现对指定为 Markov 进程代数 ROSA 进程的系统行为进行全自动化分析。在这一初步开发阶段，ROSA Analyser 能够根据 ROSA 操作语义生成标记转换系统（Labelled Transition System）。ROSA Analyser 的性能分析始于句法分析，从而生成一种分层结构，以便更便捷地应用操作语义转换规则。ROSA Analyser 能够识别比句法层面更深层次的状态等价性。这是缩减 LTS 规模进而避免状态爆炸问题、使该任务更具可处理性的首要步骤。为了更好地阐明 ROSA Analyser 的实用性，本文还提供了一个案例研究。
引用
@article{arxiv.1207.2736,
title = {ROSA Analyser: An automatized approach to analyse processes of ROSA},
author = {Raúl Pardo and Fernando L. Pelayo},
journal= {arXiv preprint arXiv:1207.2736},
year = {2012}
}
备注
In Proceedings WS-FMDS 2012, arXiv:1207.1841. Formal model's tool