New Publication: A Formal Approach for Verifying and Validating Security Objectives in Software Architecture
Our recent work on “” is now available online. This paper proposes an approach for the design and analysis of secure software architecture in the context of a component-port-connector architecture model and message passing communication. We use the Event-B formal method to create the software architecture model and security in successive steps using the refinement process. We also use proof obligations to verify the security of the successive software architecture models. Furthermore, we use the ProB model-checker and animator for the model validation. This paper was presented at the . See Publications for more details!