This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Modeling dependability features for Real-Time Embedded Systems
PrePrint
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.
Citation:
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, <http://doi.ieeecomputersociety.org/10.1109/TDSC.2014.2320714>
Usage of this product signifies your acceptance of the Terms of Use.