Title of paper: Manual for Using the UMC Model of the Automotive Case Study

Abstract

We show how to use a UMC model of the on road assistance scenario of SENSORIA's Automotive case study, described in [BGKM08], and verify properties formulated in the service-oriented temporal logic SocL.