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.
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.
Definitions
Services are typically provided by one or more servers and used by a number
of other other servers.
- service::Finite_sets=something that may or may not be provided and or used by a server.
- 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.
- For s1,s2:service, s1+s2::services= {s1, s2}.
- For S:services, s:service, S+s::services = S | {s}, set adding s to S.
Because there are only a finite number of services we can show:
- (above)|-For S1,S2:services, S1+S2 = S1 | S2.
Servers have a name, a number, provide a set of services, use a set of services, and run an operating system(os).
- server::= Net{ name:string, number:TCP_IP_Number, provides:services, using:services, os:OS}.
- servers::=@server, sets of servers.
- TCP_IP_number::= 0..255 ":" 0..255 ":" 0..255 ":" 0..255.
Domain
- domain::abbreviation=".csci.csusb.edu".
- our_numbers::@TCP_IP_number= "139:182:" 28..42 ":" 0..255.
Operating Systems
- OS::Finite_sets=Operating Systems.
- Linux::OS=Open software version of UNIX
- Solaris::OS=UNIX provided by Sun computers.
- IRIX::OS=UNIX provided by Silicon Graphics for their Indigo and Challenge computers.
- 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).
- disks::Finite_set=names for file systems that can be exported.
- |-disks={ mail, sun, sgi, linux, WEB}.
- mail::disks=users mail boxes,
- sun::disks=users home directory on Sun SPaRcs + software for Suns,
- sgi::disks=users home directory and software on Silicon Graphics Indigos,
- 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:
- files::OS->disks = following
|
|
|---|
| Linux | linux
|
| Solaris | sun
|
| IRIX | sgi
|
| AIX | ibm
|
- WEB::disks=storage for web.csusb.edu
Services
- local_login::service=Lets users in NIS login and use a machine from the console.
- DNS::service=Domain name service, finds TCP_IP_number for name and vice versa
See echo and whisper.
- NIS::service=Network Information Service, shares information - mainly about users, with other machines.
See aladdin.
- For d:disks, NFS(d)::service=Network File Service, shares disk storage across the network.
See indigo, taurus, nec363, etc.
- node::service=local login by systems administrators and local users.
- rose::service=Runs Rational Rose CASE tool, see orion.
- web::service=lets users access web.csusb.edu public directories,
- campus_login::service=permits rlogin and telnet from csusb.edu domain,
- rlogin::service=Remote login from off campus including telnet.
- ppp::service=permits access via modem using the point to point protocol,
- modem::service=permits access via a modem and terminal emulator,
- www::service=WWW server providing HTTP access to pages.
- ftp::service=FTP server.
- java1::service=Provides JDK1.0 compilers, tools, and libraries.
- java2::service=provides JDK1.1 compilers, tools, and libraries.
- java3::service=provides JDK1.2 compilers, tools, and libraries.
- POP::service=Provide EMail to remote uses via the Post Office Protocol.
- SMTP_in::service=Receives EMail using the Simple Mail Transfer Protocol.
- SMTP_out::service=Sends EMail using the Simple Mail Transfer Protocol.
- EMAIL::services= POP+SMTP_in+NFS(mail).
- email::services= SMTP_out + read_email.
- read_email::services=mailx+pine+elm.
- mailx::service=command line driven mail client lets users read and send Email.
- mailx::service=menu driven mail client lets users read and send Email.
- mailx::service=EMACS like mail client lets users read and send Email.
- oracle::service= Famous data base system.
- campus_DNS::service=provides domain name service for campus wide names.
- labs::service=lets user remotely login to a randomly selected workstation in one of our labs.
Servers
- 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 ).
- 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).
- gemini::server(name=>"gemini.csci.csusb.edu", number=>"139:182:38:??", provides=>( campus_login+java3 + oracle + web), uses=>DNS+NFS(mail)) , os=>solaris.
- 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).
- 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 ).
- echo::= the server(name=>"echo" domain, number=>"139:182:38:1", provides=>DNS, uses=>campus_DNS, os=>Linux).
- whisper::= the server(name=>"whisper" domain, number=>"139:182:38:2", provides=>DNS, uses=>campus_DNS, os=>Linux).
- aladdin::= the server(name=>"aladdin" domain, number=>"139:182:38:??", provides=>NIS, uses=> DNS, os=>Linux).
- taurus::= the server(name=>"taurus" domain, number=>"139:182:38:??", provides=>NFS(sgi)+NFS(sun), uses=> NIS+DNS, os=>solaris).
- nec363::= the server(name=>"nex363" domain, number=>"139:182:38:??", provides=>NFS(Linux)+NFS(web), uses=> NIS+DNS, os=>Linux).
- workstations::@servers=necs + sgis + dells.
The following assumptions (or axioms) define what a workstation needs and what
it does.
- |-local_login in workstations.provides.
- |-For all w:workstations, NIS and DNS in w.uses.
- |-not ( NIS in workstations.provides).
- |-not ( DNS in workstations.provides).
- |-for all d:disks, not ( NFS(d) in workstatins.provides).
- |-email in workstations.provides.
- |-For w:workstations, NFS(files(w.os)) in w.uses.
- necs::@ server, necs.os = {Linux}.
- dells::@ server, dells.os = {Linux}.
- 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.
- 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.
- (serves, MATHS)|-serves(s)= { h:server. s in h.provides }.
- (DNS, echo, whisper, serves)|- (domain_name_servers): serves(DNS) = { echo, whisper }.
- (NIS, aladdin, serves)|- (network_information_servers): serves(NIS) = { aladdin }.
- (NFS, nec365, serves)|- (file_server1): serves(NFS(linux))= {nec363}.
- (NFS, taurus, serves)|- (file_server2): serves(NFS(solaris))= {taurus}.
- (NFS, taurus, serves)|- (file_server2): serves(NFS(sgi))= {taurus}.
- more TBA
Symbols
@ Sets of, Power Set, that curly P thing in math books
$N set of objects fitting N
f=>a Ada, substitute a for f.
Glossary
- TBA::="To Be Announced".
- the N(a)::=constructor of a unique N with properties a.
- Net::=the MATHS notation for a class of structured objects or labelled n-tples.
- MATHS::=a way to express mathematical statements quickly and easily using ASCII.
[ maths ]
See Also