Information systems validation using formal models

Abstract: During the past few years, there has been growing interest to use unified modeling language (UML) to consider the functional requirements. However, lacking a tool to detect the accuracy and the logic of diagrams in this language makes a formal model indispensable. In this study, conversion of primary UML model of a system to a colored Petri net has been accomplished in order to examine the precision of the model. For this purpose, first the definition of priority and implementation tags for UML activity diagram are provided; then it is turned into colored Petri net. Second, the proposed model provides translated tags in terms of net transitions and some monitors are used to control the system characteristics. Finally, an executable model of UML activity diagram is provided so that the designer could simulate the model by using the simulation results to detect and to refine the problems of the model. In addition, by checking the results, we find out the proposed method enhances authenticity and accuracy of early models and the ratio of system validation increases compared with previous methods.

How to cite this paper

 Sarram, A & Harounabadi, A. (2014). Information systems validation using formal models.Management Science Letters , 4(3), 533-542.

Refrences

Berardi, D., Calvanese, D., & De Giacomo, G. (2005). Reasoning on UML class diagrams. Artificial Intelligence, 168(1), 70-118.

Fu, Y., He, X., Li, S.H., Dong, Z., & Bording, P.H. (2010). A model-driven approach for runtime assurance of software architecture model. International Journal of Computer and Network Security, 2(5).

Gogolla, M., Bohling, J., & Richters, M. (2005). Validating UML and OCL models in USE by automatic snapshot generation. Software & Systems Modeling, 4(4), 386-398.

Hu, Z., & Shatz, S. M. (2004, June). Mapping UML Diagrams to a Petri Net Notation for System Simulation. In SEKE (pp. 213-219).

Jensen, K., Kristensen, L. M., & Wells, L. (2007). Coloured Petri Nets and CPN Tools for modelling and validation of concurrent systems. International Journal on Software Tools for Technology Transfer, 9(3-4), 213-254.

Knapp, A., & Merz, S. (2002, June). Model checking and code generation for UML state machines and collaborations. In Proceedings of 5th Workshop on Tools for System Design and Verification, Technical Report (Vol. 11, pp. 59-64).

Kristensen, L. M., & Christensen, S. (2004). Implementing coloured Petri nets using a functional programming language. Higher-order and symbolic computation, 17(3), 207-243.

L?pez-Grao, J. P., Merseguer, J., & Campos, J. (2004). From UML activity diagrams to Stochastic Petri nets: application to software performance engineering. ACM SIGSOFT software engineering notes, 29(1), 25-36.

Ober, I., Graf, S., & Ober, I. (2006). Validating timed UML models by simulation and verification. International Journal on Software Tools for Technology Transfer, 8(2), 128-145.

Storrle, H. (2004, September). Semantics of control-flow in UML 2.0 activities. In Visual Languages and Human Centric Computing, 2004 IEEE Symposium on(pp. 235-242). IEEE.

Journals

MSL Volumes

Keywords

Authors

Countries

Management Science Letters

Information systems validation using formal models Pages 533-542 Download PDF

Add Reviews