Automated Analysis of Asynchronously Communicating Systems

详细信息    查看全文

• 刊名：Lecture Notes in Computer Science
• 出版年：2016
• 出版时间：2016
• 年：2016
• 卷：9641
• 期：1
• 页码：1-18
• 全文大小：459 KB
• 参考文献：1.Abdulla, P.A., Bouajjani, A., Jonsson, B.: On-the-fly analysis of systems with unbounded, lossy FIFO channels. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol. 1427, pp. 305–318. Springer, Heidelberg (1998)CrossRef
  2.Basu, S., Bultan, T.: Automatic verification of interactions in asynchronous systems with unbounded buffers. In: Proceedings of ASE 2014, pp. 743–754 (2014)
  3.Basu, S., Bultan, T., Ouederni, M.: Deciding choreography realizability. In: Proceedings of the POPL 2012, pp. 191–202. ACM (2012)
  4.Bennaceur, A., Chilton, C., Isberner, M., Jonsson, B.: Automated mediator synthesis: combining behavioural and ontological reasoning. In: Hierons, R.M., Merayo, M.G., Bravetti, M. (eds.) SEFM 2013. LNCS, vol. 8137, pp. 274–288. Springer, Heidelberg (2013)CrossRef
  5.Bouajjani, A., Emmi, M.: Bounded phase analysis of message-passing programs. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 451–465. Springer, Heidelberg (2012)CrossRef
  6.Bracciali, A., Brogi, A., Canal, C.: A formal approach to component adaptation. J. Softw. Syst. 74(1), 45–54 (2005)CrossRef
  7.Brand, D., Zafiropulo, P.: On communicating finite-state machines. J. ACM 30(2), 323–342 (1983)MathSciNet CrossRef MATH
  8.Brogi, A., Popescu, R.: Automated generation of BPEL adapters. In: Dan, A., Lamersdorf, W. (eds.) ICSOC 2006. LNCS, vol. 4294, pp. 27–39. Springer, Heidelberg (2006)CrossRef
  9.Bultan, T., Ferguson, C., Fu, X.: A tool for choreography analysis using collaboration diagrams. In: Proceedings of the ICWS 2009, pp. 856–863. IEEE (2009)
  10.Cámara, J., Martín, J.A., Salaün, G., Canal, C., Pimentel, E.: Semi-automatic specification of behavioural service adaptation contracts. Electr. Notes Theor. Comput. Sci. 264(1), 19–34 (2010)CrossRef
  11.Canal, C., Poizat, P., Salaün, G.: Synchronizing behavioural mismatch in software composition. In: Gorrieri, R., Wehrheim, H. (eds.) FMOODS 2006. LNCS, vol. 4037, pp. 63–77. Springer, Heidelberg (2006)CrossRef
  12.Canal, C., Poizat, P., Salaün, G.: Model-based adaptation of behavioural mismatching components. IEEE Trans. Softw. Eng. 34(4), 546–563 (2008)CrossRef
  13.Cécé, G., Finkel, A.: Verification of programs with half-duplex communication. Inf. Comput. 202(2), 166–190 (2005)MathSciNet CrossRef MATH
  14.Cubo, J., Salaün, G., Canal, C., Pimentel, E., Poizat, P.: A model-based approach to the verification and adaptation of WF/.NET components. In: Proceedings of the FACS 2007, vol. 215 of ENTCS, pp. 39–55 (2007)
  15.Darondeau, P., Genest, B., Thiagarajan, P.S., Yang, S.: Quasi-static scheduling of communicating tasks. Inf. Comput. 208(10), 1154–1168 (2010)MathSciNet CrossRef MATH
  16.Deniélou, P.-M., Yoshida, N.: Buffered communication analysis in distributed multiparty sessions. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 343–357. Springer, Heidelberg (2010)CrossRef
  17.Deniélou, P.-M., Yoshida, N.: Multiparty session types meet communicating automata. In: Seidl, H. (ed.) Programming Languages and Systems. LNCS, vol. 7211, pp. 194–213. Springer, Heidelberg (2012)CrossRef
  18.Finkel, A., McKenzie, P.: Verifying identical communicating processes is undecidable. Theor. Comput. Sci. 174(1–2), 217–230 (1997)MathSciNet CrossRef MATH
  19.Fokkink, W.: Introduction to Process Algebra. Texts in Theoretical Computer Science, 1st edn. Springer, Heidelberg (2000)CrossRef MATH
  20.X. Fu, T. Bultan, and J. Su. Analysis of Interacting BPEL Web Services. In Proc. of WWW’04, pp. 621–630. ACM Press, (2004)
  21.Fu, X., Bultan, T., Su, J.: Conversation protocols: a formalism for specification and verification of reactive electronic services. Theoret. Comput. Sci. 328(1–2), 19–37 (2004)MathSciNet CrossRef MATH
  22.Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2010: a toolbox for the construction and analysis of distributed processes. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 372–387. Springer, Heidelberg (2011)CrossRef
  23.Genest, B., Muscholl, A., Seidl, H., Zeitoun, M.: Infinite-state high-level MSCs: model-checking and realizability. J. Comput. Syst. Sci. 72(4), 617–647 (2006)MathSciNet CrossRef MATH
  24.Gierds, C., Mooij, A.J., Wolf, K.: Reducing adapter synthesis to controller synthesis. IEEE Trans. Serv. Comput. 5(1), 72–85 (2012)CrossRef
  25.Gössler, G., Salaün, G.: Realizability of choreographies for services interacting asynchronously. In: Arbab, F., Ölveczky, P.C. (eds.) FACS 2011. LNCS, vol. 7253, pp. 151–167. Springer, Heidelberg (2012)CrossRef
  26.Gouda, M.G., Manning, E.G., Yu, Y.-T.: On the progress of communications between two finite state machines. Inf. Control 63(3), 200–216 (1984)MathSciNet CrossRef MATH
  27.Güdemann, M., Salaün, G., Ouederni, M.: Counterexample guided synthesis of monitors for realizability enforcement. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol. 7561, pp. 238–253. Springer, Heidelberg (2012)CrossRef
  28.Jéron, T., Jard, C.: Testing for unboundedness of FIFO channels. Theor. Comput. Sci. 113(1), 93–117 (1993)MathSciNet CrossRef MATH
  29.Leue, S., Mayr, R., Wei, W.: A scalable incomplete test for message buffer overflow in promela models. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 216–233. Springer, Heidelberg (2004)CrossRef
  30.Leue, S., Ştefănescu, A., Wei, W.: Dependency analysis for control flow cycles in reactive communicating processes. In: Havelund, K., Majumdar, R. (eds.) SPIN 2008. LNCS, vol. 5156, pp. 176–195. Springer, Heidelberg (2008)CrossRef
  31.Martín, J.A., Pimentel, E.: Contracts for security adaptation. J. Log. Algebraic Program. 80(3–5), 154–179 (2011)CrossRef MATH
  32.Mateescu, R., Poizat, P., Salaün, G.: Adaptation of service protocols using process algebra and on-the-fly reduction techniques. In: Bouguettaya, A., Krueger, I., Margaria, T. (eds.) ICSOC 2008. LNCS, vol. 5364, pp. 84–99. Springer, Heidelberg (2008)CrossRef
  33.Nicola, R.D., Vaandrager, F.W.: Action versus state based logics for transition systems. In: Guessarian, Irène (ed.) LITP 1990. LNCS, vol. 469, pp. 407–419. Springer, Heidelberg (1990)CrossRef
  34.Ouederni, M., Salaün, G., Bultan, T.: Compatibility checking for asynchronously communicating software. In: Fiadeiro, J.L., Liu, Z., Xue, J. (eds.) FACS 2013. LNCS, vol. 8348, pp. 310–328. Springer, Heidelberg (2014)
  35.Poizat, P., Salaün, G.: Adaptation of open component-based systems. In: Bonsangue, M.M., Johnsen, E.B. (eds.) FMOODS 2007. LNCS, vol. 4468, pp. 141–156. Springer, Heidelberg (2007)CrossRef
  36.Milner, R.: Communication and Concurrency. Prentice-Hall Inc, Upper Saddle River (1989)MATH
  37.Salaün, G., Bordeaux, L., Schaerf, M.: Describing and reasoning on web services using process algebra. In: Proceedings of the ICWS 2004, pp. 43–50. IEEE Computer Society (2004)
  38.Salaün, G., Bultan, T., Roohi, N.: Realizability of choreographies using process algebra encodings. IEEE Trans. Serv. Comput. 5(3), 290–304 (2012)CrossRef
  39.Seguel, R., Eshuis, R., Grefen, P.W.P.J.: Generating minimal protocol adaptors for loosely coupled services. In: Proceedings of the ICWS 2010, pp. 417–424. IEEE CS (2010)
  40.van der Aalst, W.M.P., Mooij, A.J., Stahl, C., Wolf, K.: Service interaction: patterns, formalization, and analysis. In: Bernardo, M., Padovani, L., Zavattaro, G. (eds.) SFM 2009. LNCS, vol. 5569, pp. 42–88. Springer, Heidelberg (2009)CrossRef
  41.van Glabbeek, R.J., Weijland, W.P.: Branching time and abstraction in bisimulation semantics. J. ACM 43(3), 555–600 (1996)MathSciNet CrossRef MATH
  
• 作者单位：Lakhdar Akroun (15)
  Gwen Salaün (15)
  Lina Ye (16)
  
  15. University of Grenoble Alpes, Inria, LIG, CNRS, Grenoble, France
  16. LRI, University Paris-Sud, CentraleSupélec, CNRS, Université Paris-Saclay, Orsay, France
  
• 丛书名：Model Checking Software
• ISBN：978-3-319-32582-8
• 刊物类别：Computer Science
• 刊物主题：Artificial Intelligence and Robotics
  Computer Communication Networks
  Software Engineering
  Data Encryption
  Database Management
  Computation by Abstract Devices
  Algorithm Analysis and Problem Complexity
  
• 出版者：Springer Berlin / Heidelberg
• ISSN：1611-3349

文摘

Analyzing systems communicating asynchronously via reliable FIFO buffers is an undecidable problem. A typical approach is to check whether the system is bounded, and if not, the corresponding state space can be made finite by limiting the presence of communication cycles in behavioral models or by fixing the buffer size. In this paper, our focus is on systems that are likely to be unbounded and therefore result in infinite systems. We do not want to restrict the system by imposing any arbitrary bound. We introduce a notion of stability and prove that once the system is stable for a specific buffer bound, it remains stable whatever larger bounds are chosen for buffers. This enables one to check certain properties on the system for that bound and to ensure that the system will preserve them whatever larger bounds are used for buffers. We also prove that computing this bound is undecidable but we show how we succeed in computing these bounds for many examples using heuristics and equivalence checking.