design: | Gianfranco Ciardo |
Andrew S. Miner | |
current implementors: | Gianfranco Ciardo |
Andrew S. Miner | |
Min Wan | |
past implementors: | Ming-Ying Chung |
Robert L. Jones, III | |
Arun S. Mangalam | |
Radu I. Siminiceanu | |
Andy Jinqing Yu |
SMART is a software package that integrates various high-level logical (functional) and timing/stochastic (nonfunctional) modeling formalisms (e.g., stochastic Petri nets) in a single modeling study. Each (sub)model is described in a uniform environment and solved using a variety of solution techniques, from symbolic model-checking for temporal logic verification to numerical methods and simulation for performance analysis. Since SMART is intended as a research tool, it is written in a modular way that allows researchers to perform the easy integration of new formalisms and solution algorithms. One of the main strengths of SMART is its emphasis on structural decomposition methods for the efficient storage and analysis of discrete-state models.
Initially the acronym SMART stood for ``Simulation and Markovian Analyzer for Reliability and Timing''. However, given our emphasis on symbolic (decision-diagram-like) data structure and algorithms, we have now extended many of SMART capabilities to this area, so the acronym now stands for ``Symbolic Model checking Analyzer for Reliability and Timing''.
B. Buchholz, G. Ciardo, S. Donatelli, and P. Kemper. Complexity of memory-efficient Kronecker operations with applications to the solution of Markov models. INFORMS Journal on Computing, 13(3):203-222, 2000.
G. Ciardo and A. S. Miner. Storage alternatives for large structured state spaces. In Proc. Techniques Tools for Computer Performance Evaluation, pages 44-57 June 1997. Springer-Verlag.
A. Miner and G. Ciardo. Efficient reachability set generation and storage using decision diagrams. In Proc. ICATPN 1999, Lecture Notes in Computer Science 1639 (Proc. 20th Int. Conf. on Williamsburg, VA, USA, pages 6-25. June 1999. Springer-Verlag.
G. Ciardo and A. Miner. A data structure for the efficient Kronecker solution of GSPNs. In P. Buchholz, editor, Proc. 8th Int. Workshop on Petri Nets and Performance Models (PNPM'99), pages 22-31. Sept. 1999. IEEE Comp. Soc. Press.
A. S. Miner. Efficient solution of GSPNs using Canonical Matrix Diagrams. In Proc. 9th Int. Workshop on Petri Nets and Performance Models (PNPM'01) , pages 101-110, Aachen, Germany, Sept. 2001. IEEE Comp. Soc. Press.
G. Ciardo, G. Luettgen, and R. Siminiceanu. Efficient symbolic state-space construction for asynchronous systems. In Proc. ICATPN, pages 103-122, June 2000. Springer-Verlag.
G. Ciardo, G. Luettgen, and R. Siminiceanu. Saturation: an efficient iteration strategy for symbolic state-space generation. In Proc. TACAS, pages 328-342, April 2001. Springer-Verlag.
G. Ciardo and R. Siminiceanu. Structural symbolic CTL model checking of asynchronous systems. In Proc. CAV, LNCS 2725, pages 40-53, July 2003. Springer-Verlag.
R. L. Jones and G. Ciardo. On phased delay stochastic Petri nets: Definition and an application. In Proc. PNPM, pages 165-174, September 2001. IEEE Comp. Soc. Press.
G. Ciardo and R. Siminiceanu. Using edge-valued decision diagrams for symbolic generation of shortest paths. In Proc. FMCAD, LNCS 2517, pages 256-273, November 2002.
A. Miner, G. Ciardo, and S. Donatelli. Using the exact state space of a Markov model to compute approximate stationary measures. In Proc. SIGMETRICS, pages 207-216, June 2000. ACM Press.
G. Ciardo, R. Marmorstein, and R. Siminiceanu. Saturation unbound. In Proc. TACAS, LNCS 2619, pages 379-393, April 2003.
G. Ciardo and J. Yu. Saturation-based symbolic reachability analysis using conjunctive and disjunctive partitioning. In Proc. CHARME, October 2005.
R. Siminiceanu and G. Ciardo. Formal verification of the NASA runway safety monitor. In Proc. AVoCS, September 2004.
M.-Y. Chung and G. Ciardo. Saturation NOW. In Proc. QEST , September 2004.
M.-Y. Chung and G. Ciardo. A pattern recognition approach for speculative firing prediction in distributed saturation state-space generation. In Proc. PDMC , July 2005.
M.-Y. Chung and G. Ciardo. A dynamic firing speculation to speedup distributed symbolic state-space generation. In Proc. IPDPS , April 2006.
R. Siminiceanu and G. Ciardo. New metrics for static variable ordering in decision diagrams. In Proc. TACAS, March 2006. Springer-Verlag.
M.-Y. Chung, G. Ciardo, and J. Yu. A fine-grained fullness-guided chaining heuristic for symbolic reachability analysis. In Proc. ATVA, October 2006. Springer-Verlag.
G. Ciardo. What a structural world (Keynote Talk). In Proc. PNPM'01 , pages 3-16, September 2001. IEEE Comp. Soc. Press.
G. Ciardo, R. L. Jones, A. S. Miner, and R. Siminiceanu. Logical and stochastic modeling with SMART. In Proc. Techniques Tools for Computer Performance Evaluation, LNCS 2794, pages 78-97, September 2003. Springer-Verlag.
G. Ciardo. Reachability set generation for Petri nets: can brute force be smart? (Invited Talk). In Proc. ICATPN, pages 17-34, June 2004.
G. Ciardo, R. L. Jones, A. S. Miner, and R. Siminiceanu. Logical and stochastic modeling with SMART Performance Evaluation, vol. 63, 2006.
You can first browse the User Manual, available in PDF.
You can also browse the set of SMART examples, available as a zip archive (unpacking this zip archive will create a directory ``Examples'' and place files in it).
If the results and the capabilities demonstrated in the publications listed
above and in the manual are what you are looking for, let us hear from you by
sending us an inquiry.
Please include in your email the hardware/OS combination you need,
chosen from the following: