The existing modeling and verification methods for embedded software are insufficient towards the increasingly prominent security requirements. In this paper, aiming at high security requirements of embedded software, a security modeling and verification framework of embedded software based on semiformal and formal methods is proposed. An extensible security model ZMsec (Z-MARTE security model), which extends Z with elements of MARTE (Modeling and Analysis of Real-Time and Embedded systems) and FSA (Finite State Automata), is presented to describe three dimensions of software: security usecases, static structures and dynamic behaviors. Further on, this paper designs ZMsecTL (ZMsecTemporal Logic) formulas to describe security properties, and proposes ZMCA (ZMsec Model Checking Algorithm), a security model checking algorithm on ZMsec model, to verify security properties in ZMsecTL formulas. In order to provide an intuitive state transition diagram for model checking, a depth-first ZMsecSD (ZMsecState Diagram) generation algorithm is designed. Drawing on the abstract framework, this paper develops a prototype implementation of ZMV (ZMsec Modeling and Verification tool), a tool for ZMsec integrated with modeling and verification phases. We finally discuss an embedded software example with ZMV, which illustrates and validates the security modeling and verification method proposed in this paper. (C) 2019 Elsevier Ltd. All rights reserved.
