Please wait a minute...
FITEE
Front. Inform. Technol. Electron. Eng.  2013, Vol. 14 Issue (5): 332-346    DOI: 10.1631/jzus.C1200263
    
Validation of static properties in unified modeling language models for cyber physical systems
Gabriela Magureanu, Madalin Gavrilescu, Dan Pescaru
Department of Computers, Automation and Computers Faculty, “Politehnica University of Timisoara, Timisoara 300223, Romania
Validation of static properties in unified modeling language models for cyber physical systems
Gabriela Magureanu, Madalin Gavrilescu, Dan Pescaru
Department of Computers, Automation and Computers Faculty, “Politehnica University of Timisoara, Timisoara 300223, Romania
 全文: PDF 
摘要： 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.
关键词： Cyber physical system (CPS);  Unified modeling language (UML) design;  Formal verification;  Prototype verification system (PVS);  Z language    
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.
Key words: Cyber physical system (CPS)    Unified modeling language (UML) design    Formal verification    Prototype verification system (PVS)    Z language
收稿日期: 2012-09-15 出版日期: 2013-04-30
CLC:  TP311.5  
服务　　
把本文推荐给朋友
加入引用管理器
E-mail Alert
RSS
作者相关文章　　
Gabriela Magureanu
Madalin Gavrilescu
Dan Pescaru

引用本文:

Gabriela Magureanu, Madalin Gavrilescu, Dan Pescaru. Validation of static properties in unified modeling language models for cyber physical systems. Front. Inform. Technol. Electron. Eng., 2013, 14(5): 332-346.

链接本文:

http://www.zjujournals.com/xueshu/fitee/CN/10.1631/jzus.C1200263    或    http://www.zjujournals.com/xueshu/fitee/CN/Y2013/V14/I5/332

[1] Lam-for Kwok, Ka-shing Chan. Building an e-Portfolio with a learning plan centric approach[J]. Front. Inform. Technol. Electron. Eng., 2012, 13(1): 37-47.