Formal Specification and Transformation Method of System Requirements from B Method to AADL Model

This article presents a method to describe system requirements with B abstract machine, and transformation rules from B method to the Architecture Analysis and Design Language (AADL) model. We aim at solving the problems of requirements non-deterministic and ensuring requirements consistency during conversion procedure, AADL architecture model is consistent with requirements. Furthermore, in the early phrase of software development, various verification methods could be used to test software functional or non-functional attributes based on Model Driven Architecture (MDA). Firstly, we extract the subset of B method in this paper. Secondly, we describe this subset with formal method in terms of syntax and semantic. Thirdly, the derivation rules from B method to AADL model are proposed. The requirements consistency is then illustrated on a case study.