Validation of Bosch' Mobile Communication NetworkArchitecture with SPIN

T.C. Ruys, Romanus Langerak

    Research output: Contribution to conferencePaperpeer-review

    10 Downloads (Pure)

    Abstract

    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.
    Original languageUndefined
    Number of pages14
    Publication statusPublished - Apr 1997
    EventProceedings of SPIN97, the Third InternationalWorkshop on SPIN - Enschede, The Netherlands
    Duration: 5 Apr 19975 Apr 1997

    Workshop

    WorkshopProceedings of SPIN97, the Third InternationalWorkshop on SPIN
    Period5/04/975/04/97
    Other5 April 1997

    Keywords

    • FMT-MC: MODEL CHECKING
    • literate programming
    • IR-63314
    • Verification
    • EWI-6508
    • Promela
    • Protocol
    • SPIN
    • Model Checking
    • Validation

    Cite this