With the development of sensor network and embedded system, Cyber-Physical System (CPS) integrating computation, communication and control is becoming the focus of attention gradually. Obvious problems have emerged when CPS applying to various industries. It is crucial that the designed CPS can work as expect. A growing number of researchers are concerned about the property verification of CPS since verification technique has played a key role in improving the security and reliability of systems. It is a commonly used method that transforming generic model to formal model for verification. A formal method of theorem proving has well applied to verify CPS based on Differential Dynamic Logic (DDL) which operating model named Hybrid Program proposed by A. Platzer. This paper introduced HybridUML to model CPS, presented a method to verify CPS using DDL, where model was transformed from HybridUML to Hybrid Program, and verified a case study with the resulting model finally.
IOS Press, Inc.
6751 Tepper Drive
Clifton, VA 20124
Tel.: +1 703 830 6300
Fax: +1 703 830 2300 email@example.com
(Corporate matters and books only) IOS Press c/o Accucoms US, Inc.
For North America Sales and Customer Service
West Point Commons
Lansdale PA 19446
Tel.: +1 866 855 8967
Fax: +1 215 660 5042 firstname.lastname@example.org