Abstract
We describe the main features of Smart, a software package providing a seamless environment for the logic and probabilistic analysis of complex systems. Smart can combine different formalisms in the same modeling study. For the analysis of logical behavior, both explicit and symbolic state-space generation techniques, as well as symbolic CTL model-checking algorithms, are available. For the study of stochastic and timing behavior, both sparse-storage and Kronecker numerical solution approaches are available when the underlying process is a Markov chain. In addition, discrete-event simulation is always applicable regardless of the stochastic nature of the process, but certain classes of non-Markov models can still be solved numerically. Finally, since Smart targets both the classroom and realistic industrial settings as a learning, research, and application tool, it is written in a modular way that allows for easy integration of new formalisms and solution algorithms.
This work was partially supported by the National Aeronautics and Space Administration under NASA Contract NAG-1-2168, NAG-1-02095, and NAS-1-99124; 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 Virginia Center for Innovative Technology under grant FED-95-011.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P.: Model checking continuous-time Markov chains by transient analysis. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 358–372. Springer, Heidelberg (2000)
Bengtsson, J., et al.: New Generation of Uppaal. In: Int. Workshop on Software Tools for Technology Transfer (June 1998)
Brewer, J.W.: Kronecker products and matrix calculus in system theory. IEEE Trans. Circ. and Syst. CAS-25, 772–781 (1978)
Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comp. 35(8), 677–691 (1986)
Buchholz, P., Ciardo, G., Donatelli, S., Kemper, P.: Complexity of memory efficient Kronecker operations with applications to the solution of Markov models. INFORMS J. Comp. 12(3), 203–222 (2000)
Ciardo, G., German, R., Lindemann, C.: A characterization of the stochastic process underlying a stochastic Petri net. IEEE TSE 20(7), 506–515 (1994)
Ciardo, G., Luettgen, G., Siminiceanu, R.: Efficient symbolic state-space construction for asynchronous systems. In: Nielsen, M., Simpson, D. (eds.) ICATPN 2000. LNCS, vol. 1825, pp. 103–122. Springer, Heidelberg (2000)
Ciardo, G., Luettgen, G., Siminiceanu, R.: Saturation: An efficient iteration strategy for symbolic state space generation. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 328–342. Springer, Heidelberg (2001)
Ciardo, G., Marmorstein, R., Siminiceanu, R.: Saturation unbound. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 379–393. Springer, Heidelberg (2003) (to appear)
Ciardo, G., Miner, A.S.: Storage alternatives for large structured state spaces. In: Marie, R., Plateau, B., Calzarossa, M.C., Rubino, G.J. (eds.) TOOLS 1997. LNCS, vol. 1245, pp. 44–57. Springer, Heidelberg (1997)
Ciardo, G., Miner, A.S.: A data structure for the efficient Kronecker solution of GSPNs. In: Proc. PNPM, pp. 22–31. IEEE Comp. Soc. Press, Los Alamitos (1999)
Ciardo, G., Siminiceanu, R.: Using edge-valued decision diagrams for symbolic generation of shortest paths. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, pp. 256–273. Springer, Heidelberg (2002)
Ciardo, G., Trivedi, K.S.: A decomposition approach for stochastic reward net models. Perf. Eval. 18(1), 37–59 (1993)
Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NuSMV: a new Symbolic Model Verifier. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 495–499. Springer, Heidelberg (1999)
Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Proc. IBM Workshop on Logics of Programs, pp. 52–71 (1981)
Couvillion, J.A., et al.: Performability modeling with UltraSAN. IEEE Software, pp. 69–80 (September 1991)
Daly, D., Deavours, D.D., Doyle, J.M., Webster, P.G., Sanders, W.H.: Möbius: an extensible tool for performance and dependability modeling. In: Haverkort, B.R., Bohnenkamp, H.C., Smith, C.U. (eds.) TOOLS 2000. LNCS, vol. 1786, pp. 332–336. Springer, Heidelberg (2000)
Jones, R.L.: Analysis of Phase-Type Stochastic Petri Nets with Discrete and Continuous Timing. Tech. Rep. CR-2000-210296, NASA Langley (June 2000)
Jones, R.L., Ciardo, G.: On phased delay stochastic Petri nets: Definition and an application. In: Proc. PNPM, pp. 165–174. IEEE Computer Society Press, Los Alamitos (2001)
Jones III., R.L.: Simulation and Numerical Solution of Stochastic Petri Nets with Discrete and Continuous Timing. Ph.D. thesis, College of William and Mary, Department of Computer Science, Williamsburg, VA (2002)
Kam, T., Villa, T., Brayton, R., Sangiovanni-Vincentelli, A.: Multi-valued decision diagrams: theory and applications. Multiple-Valued Logic 4(1–2), 9–62 (1998)
Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM: Probabilistic Symbolic Model Checker. In: Proc. Comp. Perf. Eval. / TOOLS, April 2003, pp. 200–204 (2003)
Miner, A.S.: Efficient state space generation of GSPNs using decision diagrams. In: Proc. DSN, Washington, DC, June 2002, pp. 637–646 (2002)
Miner, A.S., Ciardo, G.: Efficient reachability set generation and storage using decision diagrams. In: Donatelli, S., Kleijn, J. (eds.) ICATPN 1999. LNCS, vol. 1639, pp. 6–25. Springer, Heidelberg (1999)
Miner, A.S., Ciardo, G., Donatelli, S.: Using the exact state space of a Markov model to compute approximate stationary measures. In: Proc. ACM SIGMETRICS, pp. 207–216. ACM Press, New York (2000)
Murata, T.: Petri Nets: properties, analysis and applications. Proc. of the IEEE 77(4), 541–579 (1989)
Pastor, E., Roig, O., Cortadella, J., Badia, R.: Petri net analysis using Boolean manipulation. In: Valette, R. (ed.) ICATPN 1994. LNCS, vol. 815, pp. 416–435. Springer, Heidelberg (1994)
Tilgner, M., Takahashi, Y., Ciardo, G.: SNS 1.0: Synchronized Network Solver. In: Int. Workshop on Manufacturing and Petri Nets, June 1996, pp. 215–234 (1996)
Yovine, S.: Model checking timed automata. In: European Educational Forum: School on Embedded Systems, pp. 114–152 (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ciardo, G., Jones, R.L., Miner, A.S., Siminiceanu, R. (2003). Logical and Stochastic Modeling with Smart . In: Kemper, P., Sanders, W.H. (eds) Computer Performance Evaluation. Modelling Techniques and Tools. TOOLS 2003. Lecture Notes in Computer Science, vol 2794. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45232-4_6
Download citation
DOI: https://doi.org/10.1007/978-3-540-45232-4_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40814-7
Online ISBN: 978-3-540-45232-4
eBook Packages: Springer Book Archive