Multi-models Approach for Describing and Verifying Constraints Based Interactive Systems

Authors: Mamoun Sqali, Mohamed Wassim Trojet

Abstract:

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.

Keywords: Scenarios, DEVS, synthesis, validation and verification, simulation, formal verification, z notation.

Digital Object Identifier (DOI): doi.org/10.5281/zenodo.1058889

References:

[1] ITU, 2000. Message Sequence Charts. Recommendation Z.120. International Telecommunications Union. Telecommunication Standardisation Sector.
[2] Damm, W., Harel, D., 2001. LSCs: Breathing life into message sequence charts. Formal Methods in System Design, 19(1):45--80.
[3] OMG, 2005. UML 2.0 Specification. Object Management Group. Avaibale from: http://www.omg.org
[August 2005].
[4] Brian, L., Hans, E., 2004. UML 2 toolkit. Whiley Publishing OMG press
[5] Zeigler B., 1976. Theory of Modeling and Simulation. Krieger Publishing Company. 2nd Edition. New york.
[6] Zeigler B.P., Praehofer H., Kim T. G., "Theory of Modeling and Simulation." 2nd Edition, Academic Press, New York, NY 2000.
[7] Liang H., Dingel J., Diskin Z., A comparative Survey of Scenariobased to State-based Model Synthesis Approaches, SCESM'06 : International Workshop on Scenarios and State Machines: Models, Algorithms, and Tool, Shangaï, China, pp.5-12, May 2006.
[8] David, H., Kugler, H., Pnueli, A., 2005. Synthesis Revisited: Generating Statechart Models from Scenario-Based Requirements. Formal Methods in Software and Systems Modeling.
[9] Letier, E., Kramer, J., Magee, J., Uchitel, S., 2005. Monitoring and Control in Scenario-Based Requirements Analysis. International Conference on Software Engineering, Proceedings of the 27th international conference on Software engineering.
[10] Ziadi, T., Hélou├½t, L., Jézéquel, J., 2004. Revisiting Statechart Synthesis with an Algebraic Approach. Proc. of 26th International Conference on Software Engineering (ICSE), IEEE Computer Society.p. 242-251.Edinburgh, May.
[11] Damas, C., Lambeau, B., Lamsweerde A., 2006. Scenarios, Goals, and State Machines: a Win-Win Partnershi for Model Synthesis. 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp. 197- 207. Portland, Oregon, USA.
[12] Sqali, M., Torres, L., Frydman, C., 2008. Synthèse de scénarios en DEVS, 7ème conférence internationale de Modélisation et SIMulation (MOSIM08). Paris, 31 mars-2 avril, .
[13] Sqali, M., Torres, L., Frydman, C., 2008. Synthetizing scenarios to DEVS models. SpringSim08. Ottawa, Canada.
[14] B. F. Potter, J. E. Sinclair, and D. Till. 1991. An Introduction to Formal Specification and Z. Prentice Hall International Series in Computer Science.
[15] Jonathan Bowen.Formal Specification and Documentation Using Z: A case study approach.Revised. 2003
[16] Jacky, J. 1997. The way of Z: Practical Programming with formal methods. Cambridge University Press.
[17] Peschanski, F., and D. Julien. 2003.When Concurrent Control Meets Functional Requirements, or Z+Petri-Nets." ZB 2003: Formal Specification and Development in Z and B, Springer Berlin / Heidelberg. 79-97.
[18] Trojet, M. W., A. Hamri, and C.Fydman. 2008. Logical analysis of DEVS models using Z." Proceedings of International Simulation Multi-conference ISMc'08.
[19] Felipe Cantal de Sousa, Nabor C. Mendonça, Sebastian Uchitel, Jeff Kramer "Detecting Implied Scenarios from Execution Traces", Proceedings of the 14th Working Conference on Reverse Engineering, pages: 50-59 Washington, DC, USA,2007.
[20] Muccini H., "Detecting Implied Scenarios analyzing non-local Branching Choices", Proc. Int. Conf. on Fundamental Approaches to Software Engineering, ETAPS2003, Warsaw, Poland, April 2003.
[21] M. E.-A. Hamri, G. Zacharewicz, "LSIS DME: An Environment for Modeling and Simulation of DEVS Specifications", in: AIS-CMS International modeling and simulation multiconference, pp. 55-60, Buenos Aires - Argentina, February 8-10 2007. ISBN 978-2- 9520712-6-0.