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

1994-1996

First prototype built. It contains a general framework for defining multiple interacting models that can exchange data between them. It is able to compute the stationary solution of generalized stochastic Petri net models with an ergodic underlying continuous time Markov chain using traditional sparse matrix techniques and iterative solution methods.

1997-1999

• Kronecker-based solution algorithms are integrated into SMART.

  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.

• A new data structure for state space storage using a few bytes per state is implemented. SMART computes the stationary solution of a continuous-time Markov model with 11 million states in about two days a single workstation.

  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 technique based on multiway decision diagrams (MDDs) to store the state space is implemented. When performing reachability analysis, SMART can explore and store huge state spaces using little time and memory. For example, SMART can generate the state space for the dining philosophers problem with 1,000 philosophers (almost 10**627 states) in 10 minutes using 660Kbytes of memory.

  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.

• Matrix diagrams are defined and used to store the infinitesimal generator of the underlying Markov chain. This sophisticated encoding allows SMART to employ efficient access to the entries of the infinitesimal generator by columns. SMART computes the stationary solution of a continuous-time Markov model with 40 million states in about three days, on a single workstation.

  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.

• Work begins on simulation for models with arbitrary distributions and on numerical solution of models with discrete phase-type distributions.

2000-2002

• New MDD algorithms for symbolic state-space generation are implemented, resulting in a speedup of over one order of magnitude on most models.

  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.

• A new Saturation algorithm for symbolic state-space generation is implemented, resulting in a speedup of an additional three orders of magnitude, accompanied by a similar reduction in memory requirements in many cases.

  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.

• Full CTL model checking capabilities are provided.

  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.

• A numerical solution for Phased Delay Stochastic Petri Nets (PDPNs) is implemented. This allows SMART to solve certain non-Markovian stochastic models without having to resort to discrete-event simulation.

  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.

• Efficient witness and counterexample generation for CTL model checking is provided.

  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.

• An approximation algorithm for the solution of continuous-time Markov models based on the structure of their symbolic encoding is proposed.

  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.

2003-2005

• The Saturation algorithm is extended to models where the range of the local state variables is not known a priori and then, further, to arbitrary asynchronous models that do not have to satisfy the restrictions for a Kronecker encoding of the transition relation.

  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.

• SMART is successfully used to verify NASA's Runway Safety Monitor (see http://shemesh.larc.nasa.gov/fm/fm-now-rsm.html)

  R. Siminiceanu and G. Ciardo. Formal verification of the NASA runway safety monitor. In Proc. AVoCS, September 2004.

• Works begins on a parallel/distributed implementation of the Saturation algorithm. The goal is to exploit the memory available on a network-of-workstation, to cope with the size of the decision diagrams required to study large models.

  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.

2006-2008

• Work begins on static variable ordering to reduce the size of the decision diagrams reduces reliance on user-provided information. Furthermore, in the case of Petri nets, invariants can be fully exploited to both order the model variables and reduce their number.

  R. Siminiceanu and G. Ciardo. New metrics for static variable ordering in decision diagrams. In Proc. TACAS, March 2006. Springer-Verlag.

• A fully automatic heuristic based on the idea of a fine-granularity chaining guided by the structure of the decision diagram is prototyped, showing a factor of two or more speedup on most models.

  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.

• The Saturation algorithm is modified to use edge-valued MDDs, with the goal of explore only a portion of the reachable state space. The resulting Bounded Saturation algorithm is shown to be competitive with SAT-based methods for bounded-model checking of asynchronous models.

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:

• i386-linux (this is the version with the best support)
• i386-windows
• powerpc-macOSX
• intel-macOSX

Acknowledgements