Paper Info
Title
Modeling Dependability Features for Real-Time Embedded Systems
Abstract
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.
Year
DOI
Venue
2015
10.1109/TDSC.2014.2320714
IEEE Trans. Dependable Sec. Comput.
Keywords
DocType
Volume
dependability feature modelling,z-marte,software reliability,dependability,rtes,systems analysis,real-time embedded system,formal methods,embedded systems,formal method,formal specification,real-time and embedded systems,formal verification,data models,semantics,real time systems,unified modeling language,computational modeling
Journal
12
Issue
ISSN
Citations 
2
1545-5971
4
PageRank 
References 
Authors
0.47
16
4
Name
Order
Citations
PageRank
Siru Ni1492.87
Yi Zhuang2325.08
Zining Cao34314.38
Xiangying Kong440.47