Abstract
As software systems become increasingly complex, there is growing interest in the use of formal techniques to obtain higher assurance in their correctness. The most commonly used tools involve model-checking, such as SMV and Spin. But modeling complex systems with a high degree of fidelity implies exceedingly large state spaces that must be analyzed. These state spaces are typically too large for single processing nodes, in spite of great advances in memory reduction techniques. Moreover, approximation techniques such as hash compaction are less well-received where safety-critical systems are concerned. Effective distribution of the problem over many processing nodes has the potential of supporting the huge state spaces. Since our primary interest is in safety-critical software, we have spent considerable time evaluating the performance of distributed implementations of Spin in this context. In this paper, we present our analysis of PSPIN, a distributed implementation of Spin. We identify key measures of effectiveness, and evaluate PSPIN with respect to these measures. We also present an alternative approach to partitioning that performs comparably with respect to all measures, and is up to orders of magnitude faster. Finally, we consider the question of which measures have the greatest impact on peak memory, a measure that is most critical to effective distribution.
This material is based upon work supported in part by NASA under cooperative agreement NCC-1-399.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Barnat, J., Brim, L., Stribrna, J.: Distributed LTL Model-Checking in SPIN, Technical Report FIMURS -2000-10, Faculty of Informatics, Masaryk University (2000)
Berger, M., Bokhari, S.: A Partitioning Strategy for Nonuniform Problems on Multiprocessors. IEEE Transactions on Computers C-36(5), 570–580 (1987)
Ciardo, G., German, R., Lindemann, C.: A Characterization of the Stochastic Process Underlying a Stochastic Petri Net. Software Engineering 20(7) (1994)
Cofer, D., Rangarajan, M.: Formal Modeling and Analysis of Advanced Scheduling Features in an Avionics RTOS. In: Proceedings of EMSOFT 2002: Second International Workshop on Embedded Software, Springer, Heidelberg (2002)
Demartini, C., Iosif, R., Sisto, R.: dSpin: A Dynamic Extension of SPIN. In: Dams, D.R., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol. 1680, p. 261. Springer, Heidelberg (1999)
Giannakopoulou, D., Lerda, F.: From States to Transitions: Improving Translation of LTL Formulae to Buchi Automata. In: Proc. of 22nd {IFIP} International Conference on Formal Techniques for Networked and Distributed Systems (November 2002)
Holzmann, G.J.: The Model Checker Spin. IEEE Trans. on Software Engineering 23(5), 279–295 (1997)
Honeywell: Design Description Document for the Digital Engine Operating System, Honeywell Specification no. PS7022409 (1999)
Iosif, R., Sisto, R.: Using Garbage Collection in Model Checking. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, Springer, Heidelberg (2000)
Karypis, G., Kumar, V.: METIS: A Software Package for Partitioning Unstructured Graphs, Partitioning Meshes, and Computing Fill-Reducing Orderings of Sparse Matrices, Version 4.0. Technical Report, Dept. of Computer Science, University of Minnesota (1998)
Karypis, G., Kumar, V.: Multilevel Algorithms for Multi-Constraint Graph Partitioning. In: Proceedings of Supercomputing 1998 (1998)
Lerda, F., Sisto, R.: Distributed-Memory Model Checking with Spin. In: Dams, D.R., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol. 1680, p. 22. Springer, Heidelberg (1999)
Lerda, F., Visser, W.: Addressing Dynamic Issues of Program Model Checking. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, p. 80. Springer, Heidelberg (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Rangarajan, M., Dajani-Brown, S., Schloegel, K., Cofer, D. (2004). Analysis of Distributed Spin Applied to Industrial-Scale Models. In: Graf, S., Mounier, L. (eds) Model Checking Software. SPIN 2004. Lecture Notes in Computer Science, vol 2989. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24732-6_19
Download citation
DOI: https://doi.org/10.1007/978-3-540-24732-6_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21314-7
Online ISBN: 978-3-540-24732-6
eBook Packages: Springer Book Archive