SMART: The stochastic model checking analyzer for reliability and timing

被引：0

作者：

Ciardo, G ^{[1
]}

Miner, AS ^{[1
]}

机构：

[1] Univ Calif Riverside, Riverside, CA 92521 USA

来源：

QEST 2004: FIRST INTERNATIONAL CONFERENCE ON THE QUANTITATIVE EVALUATION OF SYSTEMS, PROCEEDINGS | 2004年

关键词：

D O I：

暂无

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

SMART provides a seamless environment for the logic and probabilistic analysis of complex systems, for use in both the classroom and industrial applications. While initially designed as a powerful stochastic environment integrating multiple modeling formalisms, SMART now includes logical analysis and employs some of the most efficient data structures and algorithms for the analysis of discrete-state systems. For logical behavior explicit and symbolic state-space generation techniques and symbolic CTL modelchecking algorithms are available. For stochastic and timing behavior sparse-storage and Kronecker-based numerical solution approaches are available when the underlying process is a Markov chain, and discrete-event simulation is available for any type of underlying process. In addition, certain classes of non-Markov models can be solved numerically. For more details, see G. Ciardo et. al., "Logical and stochastic modeling with SMART", in Proc. Mod Tech. and Tools for Comp. Perf. Eval., LNCS 2794, Springer 2003, or the SMART User Manual available at http://www.cs.ucr.edu/-ciardo/SMART/.

引用

页码：338 / 339

页数：2