摘要
随机Petri网具有很强的模型描述能力,马尔可夫链是一种常用的性能分析模型.为了有效利用随机Petri网进行性能的定量分析,给出了一个详细完整的随机Petri网模型转换为同构马尔可夫链的算法.运用Floyd不变式断言法证明了算法的部分正确性,运用良序集法证明了算法的终止性.算法是部分正确的且是可终止的,这个证明结论说明算法是完全正确的.为了佐证证明结论,基于Java和SQL Server设计开发了一个软件平台,在此平台上实现了转换算法,测试实例的测试结果验证了算法的正确性.对算法时间复杂性的分析表明算法是有效的.
Stochastic Petri net has strong description ability. Markov chain is commonly used as a performance analysis model. In or- der to effectively using Stochastic Petri net to performance quantitative analysis, this paper presents a detailed and complete algodthra for converting Stochastic Petri net model to isomorphic Markov chain. The Partial correctness of the algorithm is proved by Floyd in- variant assertion method. The Termination of the algorithm is proved by well-ordered set method. The algorithm is completely cor- rect, which can be illustrated by the conclusion which is that the algorithm is partial correct and can be terminated. In order to verify the prove conclusion, the algorithm is implemented on a software platform, which is designed and developed based on Java and SQL Server. The time complexity analysis of the algorithm shows that the algorithm is effective.
出处
《小型微型计算机系统》
CSCD
北大核心
2014年第2期339-342,共4页
Journal of Chinese Computer Systems
基金
国家自然科学基金项目(91118003
61170022)资助
