Modeling and validation for embedded software confidentiality and integrity

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.