We present an approach for formal modelling of SystemC programs build uppon the “Behavior, Interactions and Priority” framework. Produced automata interactions are restricted only by using priorities rather than cutting their interactions. Produced models have thus the advantages of being composable - with other futur programs - without any change, except for the priorities. Furthermore automata are reduced by (1) collapsing all transitions inside a SystemC delta-step into a single transition before composing the automata, and (2) cuttting some interactions of private signals whitout any loss in program composability. Produced models sizes can thus be much smaller than non-reduced ones and verification speed of their properties may be much faster. We show the feasibility of the approach through the modeling, and verification of a set of SystemC benchmarks.