Validation of Bosch' Mobile Communication Network Architecture with Spin
Theo C. Ruys, Rom Langerak · University of Twente Research Information · 1997
This paper discusses validation projects carried out for the Mobile Communication Division of Robert Bosch GmbH. We verified parts of their Mobile Communication Network (MCNet), a communication system which is to be used in infotainment systems of future cars. The protocols of the MCNet have been modelled in Promela and validated with Spin. Apart from the validation results, this paper discusses some observations and recommendations of the use of Promela and Spin.