A formal analysis of a car periphery supervision system
Biniam Gebremichael, Tomas Krilavičius, Yaroslav S. Usenko · 2004
[t.krilavicius,usenko] at utwente.nl Abstract: This paper presents a formal model of the real-time service allocation unit for the Car Periphery Supervision (CPS) systema case study proposed by Robert Bosch GmbH in the context of the EU IST project AMETIST. The CPS system is a hybrid system, which is modeled in terms of timed automata. It is done by splitting the values of nonlinear continuous variables into nite set of regions and over-approximating the constraints on continuous variables into clock constraints. Safety properties of the timed model have been veried using Uppaal. This is a su±cient condition for validating the corresponding safety properties of the initial hybrid system. The di®erence in time scale between the CPS components have also been taken care of by over-approximating the timed model using the convex-hull over-approximation feature available in Uppaal.