Journal
IEEE TRANSACTIONS ON DEPENDABLE AND SECURE COMPUTING
Volume 12, Issue 2, Pages 190-203Publisher
IEEE COMPUTER SOC
DOI: 10.1109/TDSC.2014.2320714
Keywords
Dependability; formal methods; real-time and embedded systems
Categories
Funding
- National Natural Science Foundation for Youth of China [61202351]
- Aviation Science Fund of China [20128052064]
- Funding of Jiangsu Innovation Program for Graduate Education [CXLX12_0163]
Ask authors/readers for more resources
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.
Authors
I am an author on this paper
Click your name to claim this paper and add it to your profile.
Reviews
Recommended
No Data Available