Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 SMART project home page
SMART is a software package that integrates
various high-level logical and stochastic 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, including numerical methods and simulation.
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 interest in symbolic model checking, we have now extended
many of SMART capabilities to this area, so the acronym now stands for
``Stochastic Model checking Analyzer for Reliability and Timing''.
Of course, simulation capabilities an Markov models are still at the
core of SMART!
SMART milestones (in chronological order)
Spring 1994.
Work on the SMART project begins.
Spring 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.
Summer 1997.
Kronecker-based solution algorithms are being investigated for integration
in SMART.
A new data structure for state space storage using a few bytes per state
is implemented.
SMART computes the stationary solution of a model with 1.1x10**7 states
in about two days a single workstation.
Fall 1998.
A technique based on multi-valued decision diagrams (MDDs) to
store the state space is implemented.
When performing reachability analysis, SMART can now 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 (9.18x10**626 states)
in 10 minutes using 660Kbytes of memory.
Winter 1998, Spring 1999.
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 model with 4x10**7 states
in about three days, on a single workstation.
Summer 1999.
Work begins on simulation for models with arbitrary distributions
and on numerical solution of models with discrete phase-type distributions.
Summer 2000.
New MDD algorithms for symbolic state-space generation are implemented,
resulting in a speed-up of at least one order of magnitude on most
models.
Spring 2001.
A new saturation algorithm for symbolic state-space generation
is implemented, resulting in a speed-up of up to three orders of magnitude,
accompanied by a similar reduction in memory requirements in many cases.
Full CTL model checking capabilities are now provided.
Summer 2001.
A numerical solution for Phased Delay Stochastic Petri Nets (PDPNs)
is implemented.
This allows SMART to solve certain non-Markovian models without having
to resort to discrete-event simulation.
Fall 2001.
Version 1.0 released.
Fall 2002.
Version 1.1 released.
Witness and counterexample generation is now provided.
Several performance enhancements are included.
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, R. L. Jones, A. S. Miner, and R. Siminiceanu.
SMART: Stochastic Model Analyzer for Reliability and Timing
In Tools of Aachen 2001 International Multiconference on
Measurement, Modelling and Evaluation of Computer-Communication Systems,
pages 29-34, Aachen, Germany, Sept. 2001.
G. Ciardo.
Distributed and structured analysis approaches to study large and
complex systems.
In E. Brinksma, H. Hermanns, and J.-P. Katoen, editors,
Lectures on Formal Methods and Performance Analysis,
LNCS 2090, pages 344-374.
Springer-Verlag, 2001.
G. Ciardo, G. Luettgen, and R. Siminiceanu.
Saturation: an efficient iteration strategy for symbolic state-space generation.
In Proc. Tools and Algorithms for the Construction and Analysis of Systems
(TACAS 2001),
pages 328-342, Genova, Italy, Apr. 2001. Springer-Verlag.
A. Miner, G. Ciardo, and S. Donatelli.
Using the exact state space of a Markov model to compute approximate
stationary measures.
In J. Kurose and P. Nain, editors,
Proceedings of the 2000 ACM SIGMETRICS Conference on Measurement and
Modeling of Computer Systems, pages 207-216, June 2000.
ACM Press.
G. Ciardo, G. Luettgen, and Siminiceanu.
Efficient symbolic state-space construction for asynchronous systems.
In M. Nielsen and D. Simpson, editors,
Application and Theory of Petri Nets 2000,
Lecture Notes in Computer Science 1825,
(Proceedings of the 21th International Conference on
Applications and Theory of Petri Nets, Aarhus, Denmark),
pages 103-122, June 2000.
Springer-Verlag.
G. Ciardo and A. Miner.
Structural approaches for SPN analysis.
In A. Tenter, editor,
High Performance Computing 2000, Grand Challenges in
Computer Simulation, pages 345-356, Apr. 2000.
SCS.
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. 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. Miner and G. Ciardo.
Efficient reachability set generation and storage using decision diagrams.
In H. Kleijn and S. Donatelli, editors, Application and Theory of Petri Nets
1999, Lecture Notes in Computer Science 1639 (Proc. 20th Int. Conf. on
Applications and Theory of Petri Nets)
Williamsburg, VA, USA,
pages 6-25.
June 1999.
Springer-Verlag.
G. Ciardo and A. S. Miner.
SMART: Simulation and Markovian Analyzer for Reliability and Timing.
In Tools Descriptions from the
9th International Conference on Modelling Techniques
and Tools for Computer Performance Evaluation
and the 7th International Workshop on Petri Nets and Performance Models,
Saint Malo, France,
pages 41-43.
June 1997.
G. Ciardo and A. S. Miner.
Storage alternatives for large structured state spaces.
In Proc. 9th Int. Conf. on Modelling Techniques
and Tools for Computer Performance Evaluation,
St. Malo, France,
LNCS 1245,
pages 44-57
June 1997.
Springer-Verlag.
G. Ciardo and A. S. Miner.
SMART: Simulation and Markovian Analyzer for Reliability and Timing.
In Proc. IEEE International Computer Performance and
Dependability Symposium (IPDS'96), page 60, Urbana-Champaign, IL, USA.
Sept. 1996.
IEEE Comp. Soc. Press.
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
i386-solaris
sparc-solaris
powerpc-macOSX
Acknowledgements
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 and ACI-0203971;
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.
URL: http://www.cs.ucr.edu/~ciardo/SMART/index.html
Last updated: July 26, 2006.
Report suggestions and problems to:
ciardo@cs.ucr.edu