Please enable JavaScript.

Coggle requires JavaScript to display documents.

Structuring, B Model, are tighlty connected, and being performed…

- - - - Create components with independent variable sets
      - Regroup the imported component variables within a single component
    - - Workaround: merging the two components that import it
  - - - Stateless module
        
        Contains no varibles
        
        Contains sets or (abstract or concrete) constants
        
        Contains purely functional operations
        
        Imported at the highest level
        
        Can be seen from everywhere in the project
    - - Workaround: importing the seen component in the top level implementation
- - - - Traceability
    - - Simplify properties, try other modelling approaches
    - - Decompose
  - - - Max number of POs per component: 3000
    - - Decompose functions into separate modules to limit impact of modifications on the proof status
  - - - Simplify the model and decompose