[Skip Navigation] [CSUSB] / [CNS] / [CSE] / [R J Botting] / [Samples] / LOTOS
[Index] [Contents] [Source Text] [About] [Notation] [Copyright] [Comment/Contact] [Search ]
Wed Apr 25 10:31:36 PDT 2012

Opening the PDF files on this page may require you to download Adobe Reader or an equivalent viewer (GhostScript).

Contents


    LOTOS

    1. LOTOS::="ISO Standard language that combines CSP/CCS with algebraic ADT to describe telecommunication systems", [ lotos-synt.pdf ] (LOTOS Vade Mecum) [ index.php?topic=Lotos ] [ http://www.cs.stir.ac.uk/~kjt/research/well/ ] [ lookup?from=methods&search=LOTOS ]

      Formal Definition of LOTOS in MATHS

      Please Fix [click here [socket symbol] LOTOS if you can fill this hole]
    2. LOTOS::=following
      Net
      1. Process::Sets.
      2. Action::Sets.

        P,Q,R,S:Process.

        a,b,c,d:Action.

        A,B:@Action.

      3. P-a->Q::@=P can be observed executing action a and then behaving like Q.

      4. STOP::Process, takes part in no actions.
      5. |- (LOTOS_stop): for no a:Action, P:Process( STOP-a->P).

      6. δ::Action=observable termination of a Process.
      7. EXIT::Process, a process that always leads to an observable termination.
      8. |- (LOTOS_exit1): EXIT -δ->STOP.
      9. |- (LOTOS_exit2): for no a:Action~δ, P:Process( EXIT-a->P).

      10. Process Descriptions
      11. a;P::Process= a prefix P. P[>Q::Process=P disabled by Q.
      12. P|A|Q::Process=`P and Q synchonizing on A".

        Structural Operational Semantics

      13. |- (LOTOS_a2): a;P-a->P

        Rules

      14. |- (LOTOS_r1): P[>Q-a->R[>Q :- a<>δ, P-a->R.
      15. |- (LOTOS_r2): P[>Q-δ->R :- P-δ->R.
      16. |- (LOTOS_r3): P[>Q-a->R :- Q-a->R.


      17. |- (LOTOS_r4): P|A|Q-a->R|A|Q :- a not_in A| δ, P-a->R.
      18. |- (LOTOS_r5): P|A|Q-a->P|A|R :- a not_in A | δ, Q-a->R
      19. |- (LOTOS_r6): P|A|Q-a->R|A|S :- a in A | δ, a=b, P-a->R, Q-b->S.

        LOTOS example

        1. Proc::= Pdcc |ctrlc| Edcc.
        2. Pdcc::= Ping[>CtrlC.
        3. Ping::=ping; EXIT.
        4. CtrlC::=ctrlc; EXIT.
        5. Edcc::=EXIT[>CtrlC.

          then can show

        6. (above)|-Ping-ping->EXIT.


        7. (above)|-Pdcc-ping->EXIT[>CtrlC
        8. (above)|-Proc-ping->(EXIT[>CtrlC)[ctrlc]Edcc.

        . . . . . . . . . ( end of section LOTOS example) <<Contents | End>>


      (End of Net LOTOS)

    . . . . . . . . . ( end of section LOTOS) <<Contents | End>>

End