Multi-models Approach for Describing and Verifying Constraints Based Interactive Systems
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.
[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.
[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.
@article{"International Journal of Information, Control and Computer Sciences:52427", author = "Mamoun Sqali and Mohamed Wassim Trojet", title = "Multi-models Approach for Describing and Verifying Constraints Based Interactive Systems", 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.", volume = "3", number = "5", pages = "1284-11", }
