Design and formal model of an event-driven and service-oriented architecture for the Mobile Tourist Information System TIP Academic Article