Please wait a minute...
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
Download:   PDF(0KB)
Export: BibTeX | EndNote (RIS)      

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 wordsCyber physical system (CPS)      Unified modeling language (UML) design      Formal verification      Prototype verification system (PVS)      Z language     
Received: 15 September 2012      Published: 30 April 2013
CLC:  TP311.5  
Cite this article:

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.

URL:

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


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

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 
[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.