Interface Automata with Complex Actions: Limiting Interleaving in Interface Automata

• Autorzy: Esmaeilsabzali S. , Day N.A. , Mavaddat F.
• Języki publikacji: EN

Abstrakty

EN

Many formalisms use interleaving to model concurrency. To describe some system behaviours appropriately, we need to limit interleaving. For example, in a component-based system, we might wish to limit interleaving to force the inputs to a method to arrive together in order. In Web services, the arrival of XML messages consisting of multiple simple parts should not be interleaved with the behaviour of another component. We introduce interface automata with complex actions (IACA), which adds complex actions to de Alfaro and Henzinger's interface automata (IA). A complex action is a sequence of actions that may not be interleaved with actions from other components. The composition operation and refinement relation are more involved in IACA compared to IA, and we must sacrifice associativity of composition. However, we argue that the advantages of having complex actions make it a useful formalism. We provide proofs of various properties of IACA and discuss the use of IACA for modelling Web services.

• Wydawca: Polskie Towarzystwo Matematyczne
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2008
• Tom: Vol. 82, nr 4
• Strony: 465--512
• Opis fizyczny: bibliogr. 27 poz., wykr.

Twórcy

autor

Esmaeilsabzali S.

autor

Day N.A.

autor

Mavaddat F.

• David R. Cheriton School of Computer Science, University of Waterloo, Waterloo, Ontario, N2L 3G1, Canada,

Bibliografia

• [1] Aceto, L.: Action Refinement in Process Algebras, Cambridge University Press, 1992, ISBN 0-521-43111-5.
• [2] de Alfaro, L.: Game Models for Open Systems, Verification: Theory and Practice, 2772, Springer, 2003, ISBN 3-540-21002-4.
• [3] de Alfaro, L., Henzinger, T. A.: Interface Automata, Proceedings of the Joint 8th European Software Engeneering Conference and 9th ACM SIGSOFT Symposium on the Foundation of Software Engeneering (ESEC/FSE-01), 26, 5, ACM Press, 2001, ISSN 0163-5948.
• [4] de Alfaro, L., Henzinger, T. A.: Interface Theories for Component-Based Design, Proceedings of the 1st International Workshop on Embedded Software, 2211, Lecture Notes in Computer Science 2211, Springer-Verlag, 2001, ISSN 0302-9743.
• [5] de Alfaro, L., Henzinger, T. A.: Interface-Based Design, Proceedings of the Marktoberdorf Summer School, Kluwer, Engineering Theories of Software Intensive Systems, 2004.
• [6] de Alfaro, L., Stoelinga, M.: Interfaces: A Game-Theoretic Framework for Reasoning About Component-Based Systems, Electronic Notes in Theoretical Computer Science, 97, 2004, 3-23.
• [7] Alur, R., Henzinger, T. A., Kupferman, O., Vardi, M. Y.: Alternating refinement relations, Proceeding of the 9th Conference on Concurrency Theory, 1466, Springer-Verlag, 1998.
• [8] Boudol, G.: Atomic Actions (note), Bulletin of the European Association for Theoretical Computer Science, 38, 1989, 136-144, Technical Contributions.
• [9] Brzozowski, J. A.: Canonical regular expressions and minimal state graphs for definite events, in: Mathematical theory of Automata, Polytechnic Press, Polytechnic Institute of Brooklyn, N.Y., 1962, 529-561, Volume 12 of MRI Symposia Series.
• [10] Chinnici, R., Gudgin, M., Moreau, J.-J., Schlimmer, J., Weerawarana, S.: Web Services Description Language (WSDL) Version 2.0 Part 1: Core Language, 2006.
• [11] Chinnici, R., Haas, H., Moreau, J.-J., Orchard, D., Weerawarana, S.: Web Services Description Language (WSDL) Version 2.0 Part 2: Adjuncts, 2006.
• [12] Esmaeilsabzali, S., Day, N. A., Mavaddat, F.: Interface Automata with Complex Actions - Extended Version, Technical Report CS-2005-26,University ofWaterloo, David R. Cheriton School of Computer Science, 2005.
• [13] Esmaeilsabzali, S., Mavaddat, F., Day, N. A.: Interface Automata with Complex Actions, Electronic Notes in Theoretical Computer Science, 159, 2006, 79-97.
• [14] Feigenbaum, J., Kahn, J. A., Lund, C.: Complexity Results for POMSET Languages, SIAM Journal on Discrete Mathematics, 6(3), August 1993, 432-442, ISSN 0895-4801 (print), 1095-7146 (electronic).
• [15] van Glabbeek, R., Goltz, U.: Refinement of actions and equivalence notions for concurrent systems, Acta Informatica, 37(4-5), 2000, 229-327, ISSN 0001-5903.
• [16] Gorrieri, R.,Marchetti, S.,Montanari, U.: A2CCS: atomic actions for CCS, Theoretical Computer Science, 72(2-3), 1990, 203-223, ISSN 0304-3975.
• [17] Gorrieri, R., Rensink, A.: Action Refinement, in: Handbook of Process Algebra (J. A. Bergstra, A. Ponse, S. A. Smolka, Eds.), chapter 16, Elsevier, 2001, 1047-1147.
• [18] Gudgin,M., Hadley,M., Mendelsohn, N.,Moreau, J.-J., Nielsen, H. F.: SOAP Version 1.2 Part 1: Messaging Framework, W3C Recommendation, 2003.
• [19] Henzinger, T. A., Manna, Z., Pnueli, A.: An interleaving model for real time, JCIT: Proceedings of 5th Jerusalem conference on information technology, IEEE Computer Society Press, 1990, ISBN 0-8186-2078-1.
• [20] Hoare, C. A. R.: Communicating Sequential Processes, Prentice-Hall, 1985, ISBN 0-13-153271-5.
• [21] Holzmann, G. J.: The model checker Spin, IEEE Transaction on software Engineering, 23(5), 1997, 279-295, ISSN 0098-5589.
• [22] Lynch, N. A., Tuttle, M. R.: Hierarchical correctness proofs for distributed algorithms, Proceedings of the 6th ACM Symposium on Principles of Distributed Computing, ACM Press, 1987.
• [23] Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification, Springer-Verlag, 1991.
• [24] Milner, R.: Calculi of Synchrony and Asynchrony, Theoretical Computer Science, 25, 1983, 267-310.
• [25] Milner, R.: Communication and Concurrency, International Series in Computer Science, Prentice Hall, 1989.
• [26] Pratt, V. R.: Modelling Concurrency With Partial Orders, International Journal of Parallel Programming, 15(1), 1986, 33-71.
• [27] Watson, B. W.: A taxonomy of finite automata minimization algorithms, Report, Department of Mathematics and Computing Science, Eindhoven University of Technology, The Netherlands, 1994.