The automotive domain is one of the most promising areas for component and service technologies in the near future. Vehicles are increasingly becoming integrated systems where both intra-vehicle and inter-vehicles interactions require that a set of federated components (services) be properly orchestrated. The interactions and cooperations among the members of such federations suggest the use of well-known architectural styles to properly design new systems. Among the various styles, we explore the use of the publish-subscribe paradigm for intra-vehicle cooperations and the service-oriented paradigm for vehicle-to-vehicle and vehicle-to-environment interactions. We argue that available modeling notations provide adequate support to specification, but still lack proper support to the validation phase.
In this paper we discuss component models and their validation in the context of the automotive domain. In particular, we show how publish/subscribe and service-oriented applications can be analyzed through model-checking techniques by drawing simple examples from the automotive domain.