Incremental Modeling of System Architecture Satisfying SysML Functional Requirements

The aim of this work is to propose a methodological approach to model and verify Component-Based Systems (CBS), directly from SysML requirement diagrams, and to ensure formally the architecture consistency of the specified systems. The architecture consistency is guaranteed, when the components that interact in CBS are compatible and all component requirements are preserved by the composition. We propose to exploit functional requirements of CBS, specified with SysML diagrams, and the composition of components to specify incrementally system architecture. Component interfaces are specified with SysML sequence diagrams to capture their behaviors (protocols). From a requirement diagram, we associate atomic requirements, represented as LTL properties, to reusable components satisfying them. LTL properties are verified on the components with SPIN model-checker. Then, we specify system architecture incrementally, with SysML Block Definition Diagram (BDD) and Internal Block Diagram (IBD), by treating, one by one the atomic requirements.