Abstract
The execution of a reactive system amounts to the repetitions of executions of control flow cycles in the component processes of the system. The way in which cycle executions are combined is not arbitrary since cycles may depend on or exclude one another. We believe that the information of such dependencies is important to the design, understanding, and verification of reactive systems. In this paper, we formally define the concept of a cycle dependency, and propose several static analysis methods to discover such dependencies. We have implemented several strategies for computing cycle dependencies and compared their performance with realistic models of considerable size. It is also shown how the detection of accurate dependencies is used to improve a livelock freedom analysis that we developed previously.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Bradley, A.R., Manna, Z., Sipma, H.B.: Termination of polynomial programs. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 113–129. Springer, Heidelberg (2005)
Brand, D., Zafiropulo, P.: On communicating finite-state machines. Journal of the ACM 30(2), 323–342 (1983)
Cook, B., Podelski, A., Rybalchenko, A.: Abstraction refinement for termination. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 87–101. Springer, Heidelberg (2005)
Corbett, J.C., Avrunin, G.S.: Using integer programming to verify general safety and liveness properties. Formal Methods in System Design 6(1), 97–123 (1995)
Cousot, P.: Proving program invariance and termination by parametric abstraction, lagrangian relaxation and semidefinite programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 1–24. Springer, Heidelberg (2005)
Dong, Y., Du, X., Holzmann, G.J., Smolka, S.A.: Fighting livelock in the GNU i-Protocol: a case study in explicit-state model checking. Int. Journal on Software Tools for Technology Transfer (STTT) 4(4), 505–528 (2003)
Dwyer, M.B., Hatcliff, J.: Slicing software for model construction. In: Proc. of PEPM 1999, pp. 105–118 (1999)
Graham, T.C.N., Urnes, T., Nejabi, R.: Efficient distributed implementation of semi-replicated synchronous groupware. In: ACM Symposium on User Interface Software and Technology, pp. 1–10 (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. Int. Journal on Software Tools for Technology Transfer (STTT) 2(4), 394–409 (2000)
Kumar, R., Tullsen, D.: Compiling for instruction cache performance on a multithreaded architecture. In: Proc. of MICRO 2002, pp. 419–429. ACM/IEEE (2002)
Leue, S., Ştefănescu, A., Wei, W.: A livelock freedom analysis for infinite state asynchronous reactive systems. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 79–94. Springer, Heidelberg (2006)
Leue, S., Mayr, R., Wei, W.: A scalable incomplete test for the boundedness of UML RT models. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 327–341. Springer, Heidelberg (2004)
Leue, S., Wei, W.: Counterexample-based refinement for a boundedness test for CFSM languages. In: Godefroid, P. (ed.) SPIN 2005. LNCS, vol. 3639, pp. 58–74. Springer, Heidelberg (2005)
Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems – Specification. Springer, Heidelberg (1992)
Masticola, S.P., Ryder, B.G.: Non-concurrency analysis. In: PPOPP 1993, pp. 129–138. ACM Press, New York (1993)
Merino, P., Troya, J.M.: Modeling and verification of the ITU-T multipoint communication service with SPIN. In: Proc. of SPIN 1996 (1996)
Millett, L.I., Teitelbaum, T.: Issues in slicing Promela and its applications to model checking, protocol understanding, and simulation. STTT 2(4), 343–349 (2000)
Naumovich, G., Avrunin, G.S.: A conservative data flow algorithm for detecting all pairs of statements that may happen in parallel. In: SIGSOFT FSE 1998, pp. 24–34. ACM Press, New York (1998)
Nielson, F., Nielson, H.R., Hankin, C.: Principles of program analysis, 2nd edn. Springer, Heidelberg (2005)
Pelánek, R.: BEEM: Benchmarks for explicit model checkers. In: Bošnački, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 263–267. Springer, Heidelberg (2007)
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)
Ranganath, V.P., Amtoft, T., Banerjee, A., Hatcliff, J., Dwyer, M.B.: A new foundation for control dependence and slicing for modern program structures. ACM Trans. Program. Lang. Syst. 29(5) (2007)
Siegel, S.F., Avrunin, G.S.: Improving the precision of INCA by eliminating solutions with spurious cycles. IEEE Trans. Software Eng. 28(2), 115–128 (2002)
Tip, F.: A survey of program slicing techniques. Journal of Programming Languages 3(3), 121–189 (1995)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Leue, S., Ştefănescu, A., Wei, W. (2008). Dependency Analysis for Control Flow Cycles in Reactive Communicating Processes. In: Havelund, K., Majumdar, R., Palsberg, J. (eds) Model Checking Software. SPIN 2008. Lecture Notes in Computer Science, vol 5156. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-85114-1_14
Download citation
DOI: https://doi.org/10.1007/978-3-540-85114-1_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-85113-4
Online ISBN: 978-3-540-85114-1
eBook Packages: Computer ScienceComputer Science (R0)