This Article 
 Bibliographic References 
 Add to: 
Modeling dependability features for Real-Time Embedded Systems
ISSN: 1545-5971
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.
Xiangying Kong, Yi Zhuang, Zining Cao, "Modeling dependability features for Real-Time Embedded Systems," IEEE Transactions on Dependable and Secure Computing, 22 May 2014. IEEE computer Society Digital Library. IEEE Computer Society, <>
Usage of this product signifies your acceptance of the Terms of Use.