We describe the application of three formal design tools to a case study in the design of a distributed system. The case study in question involves the specification of an asynchronous message router; the three design tools are process algebra (specifically Milner's Calculus of Communicating Systems CCS), the modal μ-calculus and the Edinburgh Concurrency Workbench (CWB). We demonstrate how an informally-presented specification can be formalised within the language of the modal μ-calculus, allowing for a rigorous mathematical analysis of the correctness of our proposed implementation. For modest-sized versions of the router, this correctness proof has been carried out using the CWB.


    Zugriff

    Zugriff prüfen

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

    Asynchronous router specification


    Beteiligte:
    Moller, F. (Autor:in)

    Erschienen in:

    Erscheinungsdatum :

    1997-03-01


    Format / Umfang :

    736658 byte




    Medientyp :

    Aufsatz (Zeitschrift)


    Format :

    Elektronische Ressource


    Sprache :

    Englisch



    Asynchronous Router Specification

    Moller | Online Contents | 1997


    VOICE ROUTER

    LI CHAO / CHEN LUCAS | Europäisches Patentamt | 2016

    Freier Zugriff

    VOICE ROUTER

    LI CHAO / CHEN LUCAS | Europäisches Patentamt | 2016

    Freier Zugriff

    Voice router

    LI CHAO / CHEN LUCAS | Europäisches Patentamt | 2017

    Freier Zugriff

    SpaceWire Router

    Parkes, Steve / McClements, Chris / Kempf, Gerald et al. | BASE | 2003

    Freier Zugriff