Description
SOEN 331-S
4 System requirements
Consider a system such as flightradar24.com. A flight is associated with a flight number
(such as UA79), a specific code that an airline assigns to a particular flight in its network,
and a route which is a source-destination city pair such as (NY , Tokyo).
For example, the
United Airlines flight from New to Tokyo is tracked by the system as UA79 7→ (NY , Tokyo).
The formal specification of the system introduces the following three types:
FLIGHT NUMBER,
ROUTE,
CITY
where
ROUTE : CITY × CITY .
Flight numbers are unique, and there are possibly several flights that cover the same route.
For example, there are possibly several flights from New York to Tokyo. The system must
keep track of all active flights. Formally, let us have the following variables:
1. active: holds all active flight numbers.
2. map: holds a collection of active flight-route pairs.
5 Your assignment
1. (2 pts) Provide a declaration of variable active.
2. (3 pts) What kind of collection is variable map?
3. (10 pts) Is variable map a function and if so, comment on whether it is a total or
partial function, as well as on the properties of injectivity, surjectivity and bijectivity.
4. (10 pts) Provide a formal specification of the state of the system in terms of a Z
specification schema.
5. (15 pts) Provide a schema for operation RegisterFlightOK that adds a flight to the
tracker. With the aid of success and error schema(s), provide a definition for operation
RegisterFlight that the system will place in its exposed interface.
6. (15 pts) Provide a schema for operation GetRouteOK that returns the route given its
flight. With the aid of success and error schema(s), provide a definition for operation
GetRoute that the system will place in its exposed interface.
7. (20 pts) Provide a schema for operation GetFlightOK that returns any and all active
flights given a route. With the aid of success and error schema(s), provide a definition
for operation GetFlight that the system will place in its exposed interface.
6 What to submit
You must prepare all your solutions in LATEX and and produce a single pdf file. You may
use the .tex template provided.
Name both your .tex and .pdf assignment files after the
Concordia id of the person who will submit, e.g. 123456.pdf, and submit both .tex and .pdf
files at the Electronic Assignment Submission portal at
(https://fis.encs.concordia.ca/eas)
under Assignment 2.
END OF ASSIGNMENT.
5
