Release Time:2019-03-11  Hits:

Indexed by: Journal Article

Date of Publication: 2015-09-01

Journal: Journal of Computational Information Systems

Included Journals: Scopus、EI

Volume: 11

Issue: 17

Page Number: 6149-6157

ISSN: 15539105

Abstract: The trustworthiness of protocol is the key to ensure the reliable operation of cyber physical systems (CPS), therefore, how to design and verify protocol efficiently is unable to avoid problem in CPS design. In this paper, we propose a design method for communication protocol of CPS based on time state transition matrix (TSTM), which adds time semantics for traditional STM, making it suitable for design real-time communication protocol behavior. Then we present a model checking method based on time computation tree logic (TCTL) to verify the logical and time properties. At last, by modeling and verifying communication protocol of a type train control system, certify the effectiveness of our methods. ? 2015, by Binary Information Press