Abstract
In precursory work we suggested an abstraction-based highly scalable semi-test for the boundedness of Communicating Finite State Machine (CFSM) based modelling and programming languages. We illustrated its application to Promela and UML-RT models. The test is sound with respect to determining boundedness, but may return inconclusive ”counterexamples” when boundedness cannot be established. In this paper we turn to the question how to effectively determine the spuriousness of these counterexamples, and how to refine the abstraction based on the analysis. We employ methods from program analysis and illustrate the application of our refinement method to a number of Promela examples.
This is a preview of subscription content, log in via an institution to check access.
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
Ball, T., Podelski, A., Rajamani, S.K.: Relative completeness of abstraction refinement for software model checking. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, p. 158. Springer, Heidelberg (2002)
Bradley, A.R., Manna, Z., Sipma, H.B.: Termination of polynomial programs. In: Concurrency Theory (CONCUR) (August 2005) (to appear)
Brand, D., Zafiropulo, P.: On communicating finite-state machines. Journal of the ACM 2(5), 323–342 (1983)
Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Computer Aided Verification, pp. 154–169 (2000)
Colón, M., Sankaranarayanan, S., Sipma, H.: Linear invariant generation using non-linear constraint solving. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 420–432. Springer, Heidelberg (2003)
Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: Proceedings of the Second International Symposium on Programming, Dunod, Paris, France, pp. 106–130 (1976)
Nicholas Graham, T.C., Urnes, T., Nejabi, R.: Efficient distributed implementation of semi-replicated synchronous groupware. In: UIST 1996: Proceedings of the 9th annual ACM symposium on User interface software and technology, pp. 1–10. ACM Press, New York (1996)
Holzmann, G.J.: The Spin Model Checker - Primer and Reference Manual. Addison-Wesley, Reading (2004)
Kamel, M., Leue, S.: Formalization and validation of the General Inter-ORB Protocol (GIOP) using Promela and Spin. Software Tools for Technology Transfer 2, 394–409 (2000)
Leue, S., Mayr, R., Wei, W.: A scalable incomplete boundedness test for UML RT models. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 327–341. Springer, Heidelberg (2004)
Leue, S., Mayr, R., Wei, W.: A scalable incomplete test for buffer overflow of Promela models. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 216–233. Springer, Heidelberg (2004)
Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 239–251. Springer, Heidelberg (2004)
Podelski, A., Rybalchenko, A.: Transition invariants. In: Proc. of LICS 2004: Logic in Computer Science, pp. 32–41. IEEE, Los Alamitos (2004)
Siegel, S.F., Avrunin, G.S.: Improving the precision of inca by eliminating solutions with spurious cycles. IEEE Trans. Softw. Eng. 28(2), 115–128 (2002)
ter Beek, M.H., Massink, M., Latella, D., Gnesi, S.: Model checking groupware protocols. In: COOP, pp. 179–194 (2004)
Tip, F.: A survey of program slicing techniques. Journal of Programming Languages 3(3), 121–189 (1995)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Leue, S., Wei, W. (2005). Counterexample-Based Refinement for a Boundedness Test for CFSM Languages. In: Godefroid, P. (eds) Model Checking Software. SPIN 2005. Lecture Notes in Computer Science, vol 3639. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11537328_8
Download citation
DOI: https://doi.org/10.1007/11537328_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-28195-5
Online ISBN: 978-3-540-31899-6
eBook Packages: Computer ScienceComputer Science (R0)