[Skip Navigation] [CSUSB] / [CNS] / [Comp Sci & Eng Dept] / [R J Botting] / [Samples] / csci.csusb.edu
[Index] [Contents] [Source Text] [About] [Notation] [Copyright] [Comment/Contact] [Search ]
Tue Jun 23 10:24:15 PDT 2009


    The CSCI.CSUSB.EDU Network

      This is a demonstration of how to describe a fairly complex and real system in formal terms. It is the local csci.csusb.domain. This system has also been documented using the Unified Modelling Language (UML): [ CSciNetwork.mdl ] using Rational Rose.

      This is a snapshot of how the network used to be set up. Since then a large number of workstations and servers have been removed or changed. However, I will be fixing small technical MATHS errors.

      A network like this is a collection of hosts that act as clients and servers for various services. First we set up the formal language for talking about servers and services and then define the particular ones on this system. The users are the ultimate clients and use the local_login services.


      Services are typically provided by one or more servers and used by a number of other other servers.
    1. service::Finite_sets=something that may or may not be provided and or used by a server.
    2. services::=@service, a set of services.

      The following set up a local more readable notation for composing sets of services using a plus sign. For example this makes DNS+NIS mean a set of services comprising both DNS and NIS.

    3. For s1,s2:service, s1+s2::services= {s1, s2}.
    4. For S:services, s:service, S+s::services = S | {s}, set adding s to S.
    5. For S:services, s:service, s+S::services = S | {s}, set adding s to S.
    6. For S1:services, S2:services, S1+S2::services = S1 | S2.

      Servers have a name, a number, provide a set of services, use a set of services, and run an operating system(os).

    7. server::= Net{ name:string, number:TCP_IP_Number, provides:services, using:services, os:OS}.
    8. servers::=@server, sets of servers.

    9. TCP_IP_number::= 0..255 ":" 0..255 ":" 0..255 ":" 0..255.


    10. domain::abbreviation=".csci.csusb.edu".
    11. our_numbers::@TCP_IP_number= "139:182:" 28..42 ":" 0..255.

      Operating Systems

    12. OS::Finite_sets=Operating Systems.
    13. Linux::OS=Open software version of UNIX
    14. Solaris::OS=UNIX provided by Sun computers.
    15. IRIX::OS=UNIX provided by Silicon Graphics for their Indigo and Challenge computers.
    16. AIX::OS=UNIX provided by IBM for their RISC computers.

      File Systems

      Our users find the same environment: files and software available on all workstations of the same type, and as far as possible remotely as well. Their own files are kept on a server and accessed remotely using a Networked File System (NFS).
    17. disks::Finite_set=names for file systems that can be exported.
    18. |-disks={ mail, sun, sgi, linux, WEB}.
    19. mail::disks=users mail boxes,
    20. sun::disks=users home directory on Sun SPaRcs + software for Suns,
    21. sgi::disks=users home directory and software on Silicon Graphics Indigos,
    22. linux::disks=users home directory and software for Linux systems,

      The following documents the idea that each operating system requires a special files system for its user's home directories and binaries:

    23. files::OS->disks = following
      IRIX sgi

      (Close Table)
    24. WEB::disks=storage for web.csusb.edu


    25. local_login::service=Lets users in NIS login and use a machine from the console.
    26. DNS::service=Domain name service, finds TCP_IP_number for name and vice versa See echo and whisper.
    27. NIS::service=Network Information Service, shares information - mainly about users, with other machines. See aladdin.
    28. For d:disks, NFS(d)::service=Network File Service, shares disk storage across the network. See indigo, taurus, nec363, etc.
    29. node::service=local login by systems administrators and local users.
    30. rose::service=Runs Rational Rose CASE tool, see orion.
    31. web::service=lets users access web.csusb.edu public directories,
    32. campus_login::service=permits rlogin and telnet from csusb.edu domain,
    33. rlogin::service=Remote login from off campus including telnet.
    34. ppp::service=permits access via modem using the point to point protocol,
    35. modem::service=permits access via a modem and terminal emulator,
    36. www::service=WWW server providing HTTP access to pages.
    37. ftp::service=FTP server.
    38. java1::service=Provides JDK1.0 compilers, tools, and libraries.
    39. java2::service=provides JDK1.1 compilers, tools, and libraries.
    40. java3::service=provides JDK1.2 compilers, tools, and libraries.
    41. POP::service=Provide EMail to remote uses via the Post Office Protocol.
    42. SMTP_in::service=Receives EMail using the Simple Mail Transfer Protocol.
    43. SMTP_out::service=Sends EMail using the Simple Mail Transfer Protocol.
    44. EMAIL::services= POP+SMTP_in+NFS(mail).
    45. email::services= SMTP_out + read_email.
    46. read_email::services=mailx+pine+elm.
    47. mailx::service=command line driven mail client lets users read and send Email.
    48. mailx::service=menu driven mail client lets users read and send Email.
    49. mailx::service=EMACS like mail client lets users read and send Email.
    50. oracle::service= Famous data base system.
    51. campus_DNS::service=provides domain name service for campus wide names.
    52. labs::service=lets user remotely login to a randomly selected workstation in one of our labs.


    53. orion::= the server(name=>"orion.csci.csusb.edu", number=>"139:182:38:20", provides=>campus_login+NFS(sun) + rose + java1 + web}, uses=> DNS+NFS(mail)+NFS(WEB) , os=>solaris ).
    54. indigo::server(name=>"indigo.csci.csusb.edu", number=>"139:182:38:??", provides=>(campus_login+NFS(sgi) + java2 + web), uses=>DNS+NFS(mail)+NFS(WEB), os=>IRIX).
    55. gemini::server(name=>"gemini.csci.csusb.edu", number=>"139:182:38:??", provides=>( campus_login+java3 + oracle + web), uses=>DNS+NFS(mail)) , os=>solaris.
    56. blaze::server(name=>"blaze.csci.csusb.edu", number=>"139:182:38:??", provides=>(campus_login+ada + pascal + email ), uses=>DNS+NFS(mail)+NFS(WEB), os=AIX).
    57. dialin::= the server(name=>"dialin.csci.csusb.edu", number=>"139:182:38:??", provides=>modem+rlogin+PPP+read_email+web+labs, uses=>DNS+NIS+NFS(mail)+NFS(WEB), os=>Linux ).

    58. echo::= the server(name=>"echo" domain, number=>"139:182:38:1", provides=>DNS, uses=>campus_DNS, os=>Linux).
    59. whisper::= the server(name=>"whisper" domain, number=>"139:182:38:2", provides=>DNS, uses=>campus_DNS, os=>Linux).
    60. aladdin::= the server(name=>"aladdin" domain, number=>"139:182:38:??", provides=>NIS, uses=> DNS, os=>Linux).
    61. taurus::= the server(name=>"taurus" domain, number=>"139:182:38:??", provides=>NFS(sgi)+NFS(sun), uses=> NIS+DNS, os=>solaris).
    62. nec363::= the server(name=>"nex363" domain, number=>"139:182:38:??", provides=>NFS(Linux)+NFS(web), uses=> NIS+DNS, os=>Linux).

    63. workstations::@servers=necs + sgis + dells. The following assumptions (or axioms) define what a workstation needs and what it does.
    64. |-local_login in workstations.provides.
    65. |-For all w:workstations, NIS and DNS in w.uses.
    66. |-not ( NIS in workstations.provides).
    67. |-not ( DNS in workstations.provides).
    68. |-for all d:disks, not ( NFS(d) in workstatins.provides).
    69. |-email in workstations.provides.
    70. |-For w:workstations, NFS(files(w.os)) in w.uses.
    71. necs::@ server, necs.os = {Linux}.
    72. dells::@ server, dells.os = {Linux}.
    73. sgis::@ server, sgis.os = {IRIX}.

      Servers by service.

      This section of notes sumarizes the above information so that all the servers of a particular services are easier to find.
    74. For s:service, serves(s)::servers= s./provides, -- the set of servers that provide a given service.

      The following notation is used because the formulae are implied by the previous definitions:

       		(reasons) |- (label): conclusion.

    75. (serves, MATHS)|-serves(s)= { h:server. s in h.provides }.

    76. (DNS, echo, whisper, serves)|- (domain_name_servers): serves(DNS) = { echo, whisper }.
    77. (NIS, aladdin, serves)|- (network_information_servers): serves(NIS) = { aladdin }.
    78. (NFS, nec365, serves)|- (file_server1): serves(NFS(linux))= {nec363}.
    79. (NFS, taurus, serves)|- (file_server2): serves(NFS(solaris))= {taurus}.
    80. (NFS, taurus, serves)|- (file_server2): serves(NFS(sgi))= {taurus}.

    81. more TBA


       	@	Sets of, Power Set, that curly P thing in math books
      	$N	set of objects fitting N
       	f=>a	Ada, substitute a for f.


    82. TBA::="To Be Announced".
    83. the N(a)::=constructor of a unique N with properties a.
    84. Net::=the MATHS notation for a class of structured objects or labelled n-tples.
    85. MATHS::=a way to express mathematical statements quickly and easily using ASCII. [ maths ]

      See Also

    . . . . . . . . . ( end of section The CSCI.CSUSB.EDU Network) <<Contents | End>>