Siru Ni , Siru Ni is with the College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing, Jiangsu, 210016, China.
Ensuring dependability is significant in the development process of Real-Time Embedded Systems (RTESs). The dependability of a system model is usually presented by temporal and data constraints, which are ambiguous and incomplete when using semi-formal methods. Formal methods have precise semantics and strong verifiability, but few can capture the dependability features for RTESs. This paper presents Z-MARTE, an extensible modeling method combining MARTE profile and Z notation, to provide rigorous specifications towards the dependability features of RTESs. To extend the descriptive ability of Z, we design the time model, structure model and behavior model in Z-MARTE, specifying temporal and data constraints in the form of predicates. Z-MARTE can be edited and verified by the existing tools for Z. The converting from MARTE to Z-MARTE is supported by ZMT, a model transformation tool we design. A case study of a communication system is given to illustrate the modeling and verification procedure of Z-MARTE.
Siru Ni, Yi Zhuang, Zining Cao, Xiangying Kong, "Modeling dependability features for Real-Time Embedded Systems", IEEE Transactions on Dependable and Secure Computing, , no. 1, pp. 1, PrePrints PrePrints, doi:10.1109/TDSC.2014.2320714