Similar articles

Abstract: Cyber physical systems (CPSs) can be found nowadays in various fields of activity. The increased interest for these systems as evidenced by the large number of applications led to complex research regarding the most suitable methods for design and development. A promising solution for specification, visualization, and documentation of CPSs uses the Object Management Group (OMG) unified modeling language (UML). UML models allow an intuitive approach for embedded systems design, helping end-users to specify the requirements. However, the UML models are represented in an informal language. Therefore, it is difficult to verify the correctness and completeness of a system design. The object constraint language (OCL) was defined to add constraints to UML, but it is deficient in strict notations of mathematics and logic that permits rigorous analysis and reasoning about the specifications. In this paper, we investigated how CPS applications modeled using UML deployment diagrams could be formally expressed and verified. We used z language constructs and prototype verification system (PVS) as formal verification tools. Considering some relevant case studies presented in the literature, we investigated the opportunity of using this approach for validation of static properties in CPS UML models.

[1]Andersson, P., Host, M., 2008. UML and SystemC—a comparison and mapping rules for automatic code generation. LNEE, 10:199-209.

[2]Andre, C., Cuccuru, S., Dekeyser, J.L., de Simone, R., Dumoulin, C., Forget, J., Gautier, T., Gérard, S., Mallet, F., Radermacher, A., et al., 2005. MARTE: a New OMG Profile RFP for the Modeling and Analysis of Real-time Embedded Systems. DAC Workshop UML for SoC Design, p.16-21.

[3]Aredo, D.B., 2002. A framework for semantics of UML sequence diagrams in PVS. J. Univers. Comput. Sci., 8(7):674-698.

[4]Aredo, D.B., 2003. Formal Semantics of UML Statecharts in PVS. Proc. 7th World Multiconf. on Systemics, Cybernetics, and Informatics, Orlando, Florida, USA.

[5]Aredo, D.B., Traore, I., Stolen, K., 1999. Towards Formalization of UML Class Structure in PVS. Research Report No. 272, Department of Informatics, University of Oslo, Norway.

[6]Baar, T., 2005. Non-deterministic constructs in OCL—what does any() mean. LNCS, 3530:32-46.

[7]Bhutto, A., Hussain, D.M.A., 2011. Formal verification of UML profile. Aust. J. Basic Appl. Sci., 5(6):1594-1598.

[8]Bondavalli, A., Majzik, I., Mura, I., 1999. Automated Dependability Analysis of UML Designs. Proc. 2nd IEEE Int. Symp. on Object-Oriented Real-Time Distributed Computing, p.139-144.

[9]Buratti, C., Conti, A., Dardari, D., Verdone, R., 2009. An overview on wireless sensor networks technology and evolution. Sensors, 9(9):6869-6896.

[10]Clavel, M., Egea, M., 2006. ITP/OCL: a rewriting-based validation tool for UML+OCL static class diagrams. LNCS, 4019:368-373.

[11]Crow, J., Owre, S., Rushby, J., Shankar, N., Srivas, M., 1995. A Tutorial Introduction to PVS. Workshop on Industrial Strength Formal Specification Techniques.

[12]Derler, P., Lee, E.A., Vincentelli, A.S., 2011. Addressing Modeling Challenges in Cyber-Physical Systems. Technical Report No. UCB/EECS-2011-17, Electrical Engineering and Computer Science Department, University of California, Berkeley, USA.

[13]Dupuy, S., Ledru, Y., Chabre-Peccoud, M., 2000. An Overview of RoZ: a Tool for Integrating UML and Z Specifications. Proc. 12th Conf. on Advanced Information System Engineering, p.417-430.

[14]France, R., Evans, A., Lano, K., Rumpe, B., 1998. The UML as a formal modeling notation. Comput. Stand. Interf., 19(7):325-334.

[15]Gavrilescu, M., Magureanu, G., Pescaru, D., Jian, I., 2012. Towards UML Software Models for Cyber Physical System Applications. Proc. 20th Telecommunications Forum, p.1701-1704.

[16]Gogolla, M., Richters, M., 1998. On Constraints and Queries in UML. In: Schader, M., Korthaus, A. (Eds.), The Unified Modeling Language. Physica-Verlag, Heidelberg, Germany, p.109-121.

[17]Gogolla, M., Buttner, F., Richters, M., 2007. USE: a UML-based specification environment for validating UML and OCL. Sci. Comput. Program., 69(1-3):27-34.

[18]Hamie, A., Civello, F., Howse, J., Kent, S., Mitchell, R., 1999. Reflections on the object constraints language. LNCS, 1618:137-145.

[19]Kuzniarz, L., Staron, M., Wohlin, C., 2004. An Empirical Study on Using Stereotypes to Improve Understanding of UML Models. Proc. 12th IEEE Int. Workshop on Program Comprehension, p.14-23.

[20]Kyas, M., Fecher, H., de Boer, F.S., Jacob, J., Hooman, J., van der Zwaag, M., Arons, T., Kugler, H., 2005. Formalizing UML models and OCL sonstraints in PVS. Electron. Notes Theor. Comput. Sci., 115:39-47.

[21]Ledru, Y., 1998. Identifying Pre-conditions with the Z/EVES Theorem Prover. Proc. 13th IEEE Int. Conf. on Automated Software Engineering, p.32-41.

[22]Magureanu, G., Gavrilescu, M., Pescaru, D., Doboli, A., 2010. Towards UML Modeling of Cyber-Physical Systems: a Case Study for Gas Distribution. Proc. 8th IEEE Int. Symp. on Intelligent Systems and Informatics, p.471-476.

[23]Magureanu, G., Gavrilescu, M., Tal, I., Toma, A., Pescaru, D., Jian, I., 2011. Generating OMNeT++ Specifications from UML Models for PSoC Distributed Applications. Proc. 6th IEEE Int. Symp. on Applied Computational Intelligence and Informatics, p.85-90.

[24]Magureanu, G., Gavrilescu, M., Pescaru, D., 2012. UML Profile for Cyber-Physical System Wireless Communication Specification. Proc. 7th Int. Symp. on Applied Computational Intelligence and Informatics, p.383-388.

[25]Nguyen, K.D., Sun, Z., Thiagarajan, P.S., Wong, W.F., 2004. Model-Driven SoC Design via Executable UML to SystemC. Proc. 25th IEEE Int. Real-Time Systems Symp., p.459-468.

[26]Object Management Group (OMG), 2010. Documents Associated with UML Version 2.3 Specifications. Available from http://www.omg.org/spec/UML/2.3/ [Accessed on Dec. 26, 2012].

[27]Riccobene, E., Scandurra, P., Bocchio, S., Rosti, A., Lavazza, L., Mantellini, L., 2009. SystemC/C-based model-driven design for embedded systems. ACM Trans. Embed. Comput. Syst., 8(4):1-37.

[28]Roe, D., Broda, K., Russo, A., 2002. Mapping UML Models Incorporating OCL Constraints into Object-Z. Technical Report No. 9/2003, Imperial College, London, UK.

[29]Rousselot, J., Decotignie, J.D., 2009. A High-Precision Ultra Wideband Impulse Radio Physical Layer Model for Network Simulation. Proc. 2nd Int. Conf. on Simulation Tools and Techniques, Article No. 79.

[30]Saaltink, M., 1997. The Z/EVES system. LNCS, 1212:72-85.

[31]Shroff, M., France, R.B., 1997. Towards a Formalization of UML Class Structures in Z. Proc. 21st Int. Computer Software and Applications Conf., p.646-651.

[32]Spivey, J.M., 1992. The Z Notation: a Reference Manual (2nd Ed.). Prentice Hall International Ltd., Hertfordshire, UK.

[33]Stoyanova, T., Kerasiotis, F., Prayati, A., Papadopoulos, G., 2009. A Practical RF Propagation Model for Wireless Network Sensors. Proc. 3rd Int. Conf. on Sensor Technologies and Applications, p.194-199.