PSyHCoS: Parameter Synthesis for Hierarchical Concurrent Real-Time Systems

PSyHCoS: Parameter Synthesis for Hierarchical Concurrent Real-Time Systems
复制标题

PSyHCoS:分层并发实时系统的参数综合

DOI:
--
复制
发表时间:
2013
期刊:
International Conference on Computer Aided Verification
影响因子:
--
通讯作者:
Shang
Shang
中科院分区:
--
文献类型:
--
作者:
É. André;Yang Liu;Jun Sun;J. Dong;Shang

文献摘要

被引文献

相似文献

实时系统由于其复杂的结构、量化的时间因素、甚至未知的延迟等原因,往往难以控制。我们在这里提出PSyHCoS,用于分析参数化实时系统的工具,指定使用分层建模语言PSTCSP。PSyHCoS支持参数合成和模型检查的几种算法,以及状态空间缩减技术。它的体系结构有利于语法、语义和算法方面的可重用性。它具有友好的用户界面,可用于编辑,模拟和验证PSTCSP模型。实验证明了该方法的有效性和实用性。
Real-time systems are often hard to control, due to their complicated structures, quantitative time factors and even unknown delays. We present here PSyHCoS, a tool for analyzing parametric real-time systems specified using the hierarchical modeling language PSTCSP. PSyHCoS supports several algorithms for parameter synthesis and model checking, as well as state space reduction techniques. Its architecture favors reusability in terms of syntax, semantics, and algorithms. It comes with a friendly user interface that can be used to edit, simulate and verify PSTCSP models. Experiments show its efficiency and applicability.