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

What is SMART?

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''.

The evolution of SMART






Overview papers related to SMART

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.

How can I get SMART?

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:


This research project was partially supported by the National Aeronautics and Space Administration under NASA Contracts No. NAG-1-2168 and NAG-1-02095; by the National Science Foundation under grants CCR-0219745, ACI-0203971, CNS-0501747, and CNS-0501748; by a joint STTR project with Genoa Software Systems, Inc., for the Army Research Office; and by the matching grant FED-95-011 from the Virginia Center for Innovative Technology.

Last updated: July 23, 2008. Report suggestions and problems to: