点击次数：
所属单位：计算机科学与技术学院/人工智能学院/软件学院
发表刊物：2017 12TH INTERNATIONAL CONFERENCE ON INTELLIGENT SYSTEMS AND KNOWLEDGE ENGINEERING (IEEE ISKE)
关键字：Embedded software Confidentiality Integrity Z language Model transformation
摘要：With the rapid development of embedded software, embedded software has a highly security demand, such as confidentiality and integrity. UML provides the foundation for the construction and analysis of embedded software, but it cannot provide accurate semantics for the validation of embedded software security properties. Using the formal method based on Z language to model the security properties of embedded software, can provide the rigorous semantics for the security properties of embedded software, which can help to discover its early design errors and reduce the cost of testing and maintenance. Developing the model transformation tool of UML model to Z model, which can avoid repetitive modeling of the manual establishment of Z model, reduce the possibility of introducing artificial logic error in the model. Verifying the correctness of the confidentiality and integrity model by using the formal verification tool Z/EVES, which can make the embedded software satisfy the user's security requirement. This paper construct the static structure model and dynamic behavior model of embedded software confidentiality and integrity modeling based on Z at first; and then establish the model transformation rules of UML modeling elements to Z modeling elements, which is designed and implemented based on the XSLT technology; finally, the formal model is validated by using the verification tool Z/EVES through the example of a bicycle parking embedded software, and the correctness of the embedded software security model presented in this paper is explained.
是否译文：否
发表时间：2017-01-01
合写作者：Hu, Xinwen,曹子宁,Ye, Tong,F70206499
通讯作者：庄毅