LOTOS Code Generation for Model Checking of STBus Based SoC: the STBus interconnect