Subscribe
Issue No.03 - May/June (2010 vol.36)
pp: 390-408
Benedikt Bollig , ENS Cachan and CNRS, Cachan
Joost-Pieter Katoen , RWTH Aachen University, Aachen
Carsten Kern , RWTH Aachen University, Aachen
Martin Leucker , Technical University Munich, Munich
ABSTRACT
This paper is concerned with bridging the gap between requirements and distributed systems. Requirements are defined as basic message sequence charts (MSCs) specifying positive and negative scenarios. Communicating finite-state machines (CFMs), i.e., finite automata that communicate via FIFO buffers, act as system realizations. The key contribution is a generalization of Angluin's learning algorithm for synthesizing CFMs from MSCs. This approach is exact—the resulting CFM precisely accepts the set of positive scenarios and rejects all negative ones—and yields fully asynchronous implementations. The paper investigates for which classes of MSC languages CFMs can be learned, presents an optimization technique for learning partial orders, and provides substantial empirical evidence indicating the practical feasibility of the approach.
INDEX TERMS
Software engineering/requirements/specifications/elicitation methods, software engineering/design/design concepts, computing methodologies/artificial intelligence/learning/induction, theory of computation/computation by abstract devices/models of computation/automata.
CITATION
Benedikt Bollig, Joost-Pieter Katoen, Carsten Kern, Martin Leucker, "Learning Communicating Automata from MSCs", IEEE Transactions on Software Engineering, vol.36, no. 3, pp. 390-408, May/June 2010, doi:10.1109/TSE.2009.89
REFERENCES
 [1] B. Adsul, M. Mukund, K.N. Kumar, and V. Narayanan, "Causal Closure for MSC Languages," Foundations of Software Technology and Theoretical Computer Science, pp. 335-347, Springer, 2005. [2] R. Alur, K. Etessami, and M. Yannakakis, "Inference of Message Sequence Charts," IEEE Trans. Software Eng., vol. 29, no. 7, pp. 623-633, July 2003. [3] R. Alur, K. Etessami, and M. Yannakakis, "Realizability and Verification of MSC Graphs," Theoretical Computer Science, vol. 331, no. 1, pp. 97-114, 2005. [4] D. Angluin, "Learning Regular Sets from Queries and Counterexamples," Information and Computation, vol. 75, no. 2, pp. 87-106, 1987. [5] J. Araújo, "Formalizing Sequence Diagrams," Proc. OOPSLA Workshop Formalizing UML. Why? How? 1998. [6] N. Baudru and R. Morin, "Safe Implementability of Regular Message Sequence Chart Specifications," Software Eng., Artificial Intelligence, Networking and Parallel/Distributed Computing, pp. 210-217, Springer, 2003. [7] N. Baudru and R. Morin, "Synthesis of Safe Message-Passing Systems," Foundations of Software Technology and Theoretical Computer Science, pp. 277-289, Springer, 2007. [8] B. Bollig, J.-P. Katoen, C. Kern, and M. Leucker, "Replaying Play in and Play Out: Synthesis of Design Models from Scenarios by Learning," Tools and Algorithms for the Construction and Analysis of Systems, pp. 435-450, Springer, 2007. [9] B. Bollig, J.-P. Katoen, C. Kern, and M. Leucker, "Smyle: A Tool for Synthesizing Distributed Models from Scenarios by Learning," CONCUR 2008—Concurrency Theory, pp. 162-166, Springer, 2008. [10] B. Bollig, J.-P. Katoen, C. Kern, and M. Leucker, "SMA—The Smyle Modeling Approach," Proc. Third IFIP TC2 Central and East European Conf. Software Eng. Techniques), 2009. [11] B. Bollig, D. Kuske, and I. Meinecke, "Propositional Dynamic Logic for Message-Passing Systems," Foundations of Software Technology and Theoretical Computer Science, pp. 303-315, Springer, 2007. [12] B. Bollig and M. Leucker, "A Hierarchy of Implementable MSC Languages," Formal Techniques for Networked and Distributed Systems, pp. 53-67, Springer, 2005. [13] D. Brand and P. Zafiropulo, "On Communicating Finite-State Machines," J. ACM, vol. 30, no. 2, pp. 323-342, 1983. [14] E. Chang and R. Roberts, "An Improved Algorithm for Decentralized Extrema-Finding in Circular Configurations of Processes," Comm. ACM, vol. 22, no. 5, pp. 281-283, 1979. [15] J.E. Cook and A.L. Wolf, "Discovering Models of Software Processes from Event-Based Data," ACM Trans. Software Eng. and Methodology, vol. 7, no. 3, pp. 215-249, 1998. [16] C. Damas, B. Lambeau, and P. Dupont, "Generating Annotated Behavior Models from End-User Scenarios," IEEE Trans. Software Eng., vol. 31, no. 12, pp. 1056-1073, Dec. 2005. [17] W. Damm and D. Harel, "LSCs: Breathing Life into Message Sequence Charts," Formal Methods in System Design, vol. 19, no. 1, pp. 45-80, 2001. [18] D. Harel and R. Marelly, Come, Let's Play: Scenario-Based Programming Using LSCs and the Play-Engine. Springer, 2003. [19] P. Dupont, "Incremental Regular Inference," Proc. Int'l Coll. Grammatical Inference: Learning Syntax from Sentences, L. Miclet and C. de la Higuera, eds., pp. 222-237, 1996. [20] E. Elkind, B. Genest, D. Peled, and H. Qu, "Grey-Box Checking," Formal Techniques for Networked and Distributed Systems, pp. 420-435, Springer, 2006. [21] U. Endriss, N. Maudet, F. Sadri, and F. Toni, "Logic-Based Agent Communication Protocols," Proc. Workshop Agent Comm. Languages, pp. 91-107, 2003. [22] U. Endriss, N. Maudet, F. Sadri, and F. Toni, "Protocol Conformance for Logic-Based Agents," Proc. Int'l Joint Conf. Artificial Intelligence, pp. 679-684, 2003. [23] B. Genest, "Compositional Message Sequence Charts (CMSCs) Are Better to Implement than MSCs," Tools and Algorithms for the Construction and Analysis of Systems, pp. 429-444, Springer, 2005. [24] B. Genest, D. Kuske, and A. Muscholl, "A Kleene Theorem and Model Checking Algorithms for Existentially Bounded Communicating Automata," Information and Computation, vol. 204, no. 6, pp. 920-956, 2006. [25] B. Genest, D. Kuske, and A. Muscholl, "On Communicating Automata with Bounded Channels," Fundamentals of Information, vol. 80, no. 2, pp. 147-167, 2007. [26] B. Genest, A. Muscholl, H. Seidl, and M. Zeitoun, "Infinite-State High-Level MSCs: Model-Checking and Realizability," J. Computing and System Sciences, vol. 72, no. 4, pp. 617-647, 2006. [27] J.G. Henriksen, M. Mukund, K.N. Kumar, M. Sohoni, and P.S. Thiagarajan, "A Theory of Regular MSC Languages," Information Computing, vol. 202, no. 1, pp. 1-38, 2005. [28] H. Hungar, O. Niese, and B. Steffen, "Domain-Specific Optimization in Automata Learning," Computer Aided Verification, pp. 315-327, Springer, 2003. [29] ITU-TS Recommendation Z.120anb: Formal Semantics of Message Sequence Charts, 1998. [30] ITU-TS Recommendation Z.120 (04/04): Message Sequence Chart, 2004. [31] I. Krüger, R. Grosu, P. Scholz, and M. Broy, "From MSCs to Statecharts," Proc. IFIP Conf. Distributed and Parallel Embedded Systems, vol. 155, pp. 61-72, 1998. [32] M. Lohrey, "Realizability of High-Level Message Sequence Charts: Closing the Gaps," Theoretical Computer Science, vol. 309, nos. 1-3, pp. 529-554, 2003. [33] E. Mäkinen and T. Systä, "MAS—an Interactive Synthesizer to Support Behavioral Modeling in UML," Proc. Int'l Conf. Software Eng., pp. 15-24, 2001. [34] A.L. Martins, H.S. Pinto, and A.L. Oliveira, "Using a More Powerful Teacher to Reduce the Number of Queries of the ${\rm L}^\ast$ Algorithm in Practical Applications," Proc. Portuguese Conf. Artificial Intelligence, pp. 325-336, 2005. [35] R. Morin, "Recognizable Sets of Message Sequence Charts," Proc. Ann. Symp. Theoretical Aspects of Computer Science, pp. 523-534, 2002. [36] B. Nuseibeh and S. Easterbrook, "Requirements Engineering: A Roadmap," Proc. Int'l Conf. Software Eng., pp. 35-46, 2000. [37] J. Oncina and P. García, "Inferring Regular Languages in Polynomial Updated Time," Proc. Fourth Spanish Symp. Pattern Recognition and Image Analysis, vol. 1, pp. 49-61, 1992. [38] B. Sengupta and R. Cleaveland, "Triggered Message Sequence Charts," IEEE Trans. Software Eng., vol. 32, no. 8, pp. 587-607, Aug. 2006. [39] A.S. Tanenbaum, Computer Networks. Prentice Hall, 2002. [40] S. Uchitel, G. Brunet, and M. Chechik, "Behaviour Model Synthesis from Properties and Scenarios," Proc. Int'l Conf. Software Eng., pp. 34-43, 2007. [41] S. Uchitel, J. Kramer, and J. Magee, "Synthesis of Behavioral Models from Scenarios," IEEE Trans. Software Eng., vol. 29, no. 2, pp. 99-115, Feb. 2003.