Validation of static properties in unified modeling language models for cyber physical systems

Gabriela MAGUREANU; Madalin GAVRILESCU; Dan PESCARU

doi:10.1631/jzus.C1200263

Your Location：

Home >

Browse articles >

Validation of static properties in unified modeling language models for cyber physical systems

Computer Engineering | Updated：2022-12-09

- Validation of static properties in unified modeling language models for cyber physical systems
- Validation of static properties in unified modeling language models for cyber physical systems
- Frontiers of Information Technology & Electronic Engineering Vol. 14, Issue 5, Pages: 332-346(2013)
- Affiliations：
  
  Department of Computers, Automation and Computers Faculty, "Politehnica" University of Timisoara, Timisoara 300223, Romania
- Author bio：
  
  [ "Gabriela MAGUREANU, E-mail: gabriela_magureanu@yahoo.com" ]
- Funds：
- DOI：10.1631/jzus.C1200263
  CLC： TP311.5
- Received：15 September 2012，
  
  Revised：2013-;3-;6，
  
  Published：2013-05
- Accepted：
Scan QR Code
Gabriela MAGUREANU, Madalin GAVRILESCU, Dan PESCARU. Validation of static properties in unified modeling language models for cyber physical systems[J]. Frontiers of Information Technology & Electronic Engineering, 2013, 14(5): 332-346.
DOI：

Gabriela MAGUREANU, Madalin GAVRILESCU, Dan PESCARU. Validation of static properties in unified modeling language models for cyber physical systems[J]. Frontiers of Information Technology & Electronic Engineering, 2013, 14(5): 332-346. DOI： 10.1631/jzus.C1200263.

摘要

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.

关键词

Keywords

references

P. Andersson , , , M. Host . . UML and SystemC—a comparison and mapping rules for automatic code generation . . LNEE , , 2008 . . 10 199 - - 209 . . DOI: 10.1007/978-1-4020-8297-9_14 http://doi.org/10.1007/978-1-4020-8297-9_14 . .

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

D.B. Aredo . . A framework for semantics of UML sequence diagrams in PVS . . J. Univers. Comput. Sci. , , 2002 . . 8 ( ( 7 ): ): 674 - - 698 . . DOI: 10.3217/jucs-008-07 http://doi.org/10.3217/jucs-008-07 . .

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

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

T. Baar . . Non-deterministic constructs in OCL—what does any() mean . . LNCS , , 2005 . . 3530 32 - - 46 . . DOI: 10.1007/11506843_3 http://doi.org/10.1007/11506843_3 . .

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

A. Bondavalli , , , I. Majzik , , , I. Mura . . Automated Dependability Analysis of UML Designs . . Proc. 2nd IEEE Int. Symp. on Object-Oriented Real-Time Distributed Computing , , 1999 . . p.139 - - 144 . . DOI: 10.1109/ISORC.1999.776367 http://doi.org/10.1109/ISORC.1999.776367 . .

C. Buratti , , , A. Conti , , , D. Dardari , , , R. Verdone . . An overview on wireless sensor networks technology and evolution . . Sensors , , 2009 . . 9 ( ( 9 ): ): 6869 - - 6896 . . DOI: 10.3390/s90906869 http://doi.org/10.3390/s90906869 . .

M. Clavel , , , M. Egea . . ITP/OCL: a rewriting-based validation tool for UML+OCL static class diagrams . . LNCS , , 2006 . . 4019 368 - - 373 . . DOI: 10.1007/11784180_28 http://doi.org/10.1007/11784180_28 . .

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

P. Derler , , , E.A. Lee , , , A.S. Vincentelli . . 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 , , 2011 . . .

S. Dupuy , , , Y. Ledru , , , M. Chabre-Peccoud . . An Overview of RoZ: a Tool for Integrating UML and Z Specifications . . Proc. 12th Conf. on Advanced Information System Engineering , , 2000 . . p.417 - - 430 . . DOI: 10.1007/3-540-45140-4_28 http://doi.org/10.1007/3-540-45140-4_28 . .

R. France , , , A. Evans , , , K. Lano , , , B. Rumpe . . The UML as a formal modeling notation . . Comput. Stand. Interf. , , 1998 . . 19 ( ( 7 ): ): 325 - - 334 . . DOI: 10.1016/S0920-5489(98)00020-8 http://doi.org/10.1016/S0920-5489(98)00020-8 . .

M. Gavrilescu , , , G. Magureanu , , , D. Pescaru , , , I. Jian . . Towards UML Software Models for Cyber Physical System Applications . . Proc. 20th Telecommunications Forum , , 2012 . . p.1701 - - 1704 . . DOI: 10.1109/TELFOR.2012.6419554 http://doi.org/10.1109/TELFOR.2012.6419554 . .

M. Gogolla , , , M. Richters . . On Constraints and Queries in UML . . In: Schader M., Korthaus, A. (Eds.), The Unified Modeling Language. Physica-Verlag, Heidelberg, Germany , , 1998 . . p.109 - - 121 . . DOI: 10.1007/978-3-642-48673-9_8 http://doi.org/10.1007/978-3-642-48673-9_8 . .

M. Gogolla , , , F. Buttner , , , M. Richters . . USE: a UML-based specification environment for validating UML and OCL . . Sci. Comput. Program. , , 2007 . . 69 ( ( 1-3 ): ): 27 - - 34 . . DOI: 10.1016/j.scico.2007.01.013 http://doi.org/10.1016/j.scico.2007.01.013 . .

A. Hamie , , , F. Civello , , , J. Howse , , , S. Kent , , , R. Mitchell . . Reflections on the object constraints language . . LNCS , , 1999 . . 1618 137 - - 145 . . DOI: 10.1007/978-3-540-48480-6_13 http://doi.org/10.1007/978-3-540-48480-6_13 . .

L. Kuzniarz , , , M. Staron , , , C. Wohlin . . An Empirical Study on Using Stereotypes to Improve Understanding of UML Models . . Proc. 12th IEEE Int. Workshop on Program Comprehension , , 2004 . . p.14 - - 23 . . DOI: 10.1109/WPC.2004.1311043 http://doi.org/10.1109/WPC.2004.1311043 . .

M. Kyas , , , H. Fecher , , , F.S. de Boer , , , J. Jacob , , , J. Hooman , , , M. van der Zwaag , , , T. Arons , , , H. Kugler . . Formalizing UML models and OCL sonstraints in PVS . . Electron. Notes Theor. Comput. Sci. , , 2005 . . 115 39 - - 47 . . DOI: 10.1016/j.entcs.2004.09.027 http://doi.org/10.1016/j.entcs.2004.09.027 . .

Y. Ledru . . Identifying Pre-conditions with the Z/EVES Theorem Prover . . Proc. 13th IEEE Int. Conf. on Automated Software Engineering , , 1998 . . p.32 - - 41 . . DOI: 10.1109/ASE.1998.732566 http://doi.org/10.1109/ASE.1998.732566 . .

G. Magureanu , , , M. Gavrilescu , , , D. Pescaru , , , A. Doboli . . Towards UML Modeling of Cyber-Physical Systems: a Case Study for Gas Distribution . . Proc. 8th IEEE Int. Symp. on Intelligent Systems and Informatics , , 2010 . . p.471 - - 476 . . DOI: 10.1109/SISY.2010.5647314 http://doi.org/10.1109/SISY.2010.5647314 . .

G. Magureanu , , , M. Gavrilescu , , , I. Tal , , , A. Toma , , , D. Pescaru , , , I. Jian . . Generating OMNeT++ Specifications from UML Models for PSoC Distributed Applications . . Proc. 6th IEEE Int. Symp. on Applied Computational Intelligence and Informatics , , 2011 . . p.85 - - 90 . . DOI: 10.1109/SACI.2011.5872977 http://doi.org/10.1109/SACI.2011.5872977 . .

G. Magureanu , , , M. Gavrilescu , , , D. Pescaru . . UML Profile for Cyber-Physical System Wireless Communication Specification . . Proc. 7th Int. Symp. on Applied Computational Intelligence and Informatics , , 2012 . . p.383 - - 388 . . DOI: 10.1109/SACI.2012.6250034 http://doi.org/10.1109/SACI.2012.6250034 . .

K.D. Nguyen , , , Z. Sun , , , P.S. Thiagarajan , , , W.F. Wong . . Model-Driven SoC Design via Executable UML to SystemC . . Proc. 25th IEEE Int. Real-Time Systems Symp. , , 2004 . . p.459 - - 468 . . DOI: 10.1109/REAL.2004.32 http://doi.org/10.1109/REAL.2004.32 . .

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

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

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

J. Rousselot , , , J.D. Decotignie . . 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 , , 2009 . . DOI: 10.4108/ICST.SIMUTOOLS2009.5628 http://doi.org/10.4108/ICST.SIMUTOOLS2009.5628 . .

M. Saaltink . . The Z/EVES system . . LNCS , , 1997 . . 1212 72 - - 85 . . DOI: 10.1007/BFb0027284 http://doi.org/10.1007/BFb0027284 . .

M. Shroff , , , R.B. France . . Towards a Formalization of UML Class Structures in Z . . Proc. 21st Int. Computer Software and Applications Conf. , , 1997 . . p.646 - - 651 . . DOI: 10.1109/CMPSAC.1997.625087 http://doi.org/10.1109/CMPSAC.1997.625087 . .

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

T. Stoyanova , , , F. Kerasiotis , , , A. Prayati , , , G. Papadopoulos . . A Practical RF Propagation Model for Wireless Network Sensors . . Proc. 3rd Int. Conf. on Sensor Technologies and Applications , , 2009 . . p.194 - - 199 . . DOI: 10.1109/SENSORCOMM.2009.39 http://doi.org/10.1109/SENSORCOMM.2009.39 . .

Views

Downloads

CSCD

Alert me when the article has been cited

Submit

Tools

Publicity Resources

No data

Related Author

No data

Related Institution

No data

Chat

Address：Zhejiang University Press, 148 Tianmushan Road, Hangzhou, China Postal code：310028
Tel：+86-571-88273162 Email：fitee@zju.edu.cn
It is recommended to read the content of this site in Chrome&IE9+. Please switch to extreme mode in browser 360.
Cookies We use cookies to help provide and enhance our service and tailor content. By continuing, you agree to the use of cookies.

⁰