An Event-B Based Approach to Model and Verify Behaviors for Component-Based Applications