The requirements analysis, modeling, and simulation have consistently been one of the main challenges during the development of complex systems. The scenarios and the state machines are two successful models to describe the behavior of an interactive system. The scenarios represent examples of system execution in the form of sequences of messages exchanged between objects and are a partial view of the system. In contrast, state machines can represent the overall system behavior. The automation of processing scenarios in the state machines provide some answers to various problems such as system behavior validation and scenarios consistency checking. In this paper, we propose a method for translating scenarios in state machines represented by Discreet EVent Specification and procedure to detect implied scenarios. Each induced DEVS model represents the behavior of an object of the system. The global system behavior is described by coupling the atomic DEVS models and validated through simulation. We improve the validation process with integrating formal methods to eliminate logical inconsistencies in the global model. For that end, we use the Z notation., {"references":["ITU, 2000. Message Sequence Charts. Recommendation Z.120.\nInternational Telecommunications Union. Telecommunication\nStandardisation Sector.","Damm, W., Harel, D., 2001. LSCs: Breathing life into message\nsequence charts. Formal Methods in System Design, 19(1):45--80.","OMG, 2005. UML 2.0 Specification. Object Management Group.\nAvaibale from: http://www.omg.org [August 2005].","Brian, L., Hans, E., 2004. UML 2 toolkit. Whiley Publishing OMG\npress","Zeigler B., 1976. Theory of Modeling and Simulation. Krieger\nPublishing Company. 2nd Edition. New york.","Zeigler B.P., Praehofer H., Kim T. G., \"Theory of Modeling and\nSimulation.\" 2nd Edition, Academic Press, New York, NY 2000.","Liang H., Dingel J., Diskin Z., A comparative Survey of Scenariobased\nto State-based Model Synthesis Approaches, SCESM'06 :\nInternational Workshop on Scenarios and State Machines: Models,\nAlgorithms, and Tool, Shangaï, China, pp.5-12, May 2006.","David, H., Kugler, H., Pnueli, A., 2005. Synthesis Revisited:\nGenerating Statechart Models from Scenario-Based Requirements.\nFormal Methods in Software and Systems Modeling.","Letier, E., Kramer, J., Magee, J., Uchitel, S., 2005. Monitoring and\nControl in Scenario-Based Requirements Analysis. International\nConference on Software Engineering, Proceedings of the 27th\ninternational conference on Software engineering.\n[10] Ziadi, T., Hélou├½t, L., Jézéquel, J., 2004. Revisiting Statechart\nSynthesis with an Algebraic Approach. Proc. of 26th International\nConference on Software Engineering (ICSE), IEEE Computer\nSociety.p. 242-251.Edinburgh, May.\n[11] Damas, C., Lambeau, B., Lamsweerde A., 2006. Scenarios, Goals,\nand State Machines: a Win-Win Partnershi for Model Synthesis. 14th\nACM SIGSOFT International Symposium on Foundations of\nSoftware Engineering, pp. 197- 207. Portland, Oregon, USA.\n[12] Sqali, M., Torres, L., Frydman, C., 2008. Synthèse de scénarios en\nDEVS, 7ème conférence internationale de Modélisation et\nSIMulation (MOSIM08). Paris, 31 mars-2 avril, .\n[13] Sqali, M., Torres, L., Frydman, C., 2008. Synthetizing scenarios to\nDEVS models. SpringSim08. Ottawa, Canada.\n[14] B. F. Potter, J. E. Sinclair, and D. Till. 1991. An Introduction to\nFormal Specification and Z. Prentice Hall International Series in\nComputer Science.\n[15] Jonathan Bowen.Formal Specification and Documentation Using Z:\nA case study approach.Revised. 2003\n[16] Jacky, J. 1997. The way of Z: Practical Programming with formal\nmethods. Cambridge University Press.\n[17] Peschanski, F., and D. Julien. 2003.When Concurrent Control Meets\nFunctional Requirements, or Z+Petri-Nets.\" ZB 2003: Formal\nSpecification and Development in Z and B, Springer Berlin /\nHeidelberg. 79-97.\n[18] Trojet, M. W., A. Hamri, and C.Fydman. 2008. Logical analysis of\nDEVS models using Z.\" Proceedings of International Simulation\nMulti-conference ISMc'08.\n[19] Felipe Cantal de Sousa, Nabor C. Mendon├ºa, Sebastian Uchitel, Jeff\nKramer \"Detecting Implied Scenarios from Execution Traces\",\nProceedings of the 14th Working Conference on Reverse\nEngineering, pages: 50-59 Washington, DC, USA,2007.\n[20] Muccini H., \"Detecting Implied Scenarios analyzing non-local\nBranching Choices\", Proc. Int. Conf. on Fundamental Approaches to\nSoftware Engineering, ETAPS2003, Warsaw, Poland, April 2003.\n[21] M. E.-A. Hamri, G. Zacharewicz, \"LSIS DME: An Environment for\nModeling and Simulation of DEVS Specifications\", in: AIS-CMS\nInternational modeling and simulation multiconference, pp. 55-60,\nBuenos Aires - Argentina, February 8-10 2007. ISBN 978-2-\n9520712-6-0."]}