Requirements Checking Assignment 

Practical Information

  • Due Date: Friday 21 October 2022, before 23:59.
  • Team Size: 2 (pair design/programming)!
    Note that as of the 2017-2018 Academic Year, each International student should team up with "local" (i.e., whose Bachelor degree was obtained at the University of Antwerp).
  • Submission Information: Only one member of each team submits a full solution. This must be a compressed archive (ZIP, RAR, TAR.GZ...) that includes your report and all models, images, code and other sources that you have used to crate your solution. Do not submit any executables. The report may be either HTML or PDF and must be accompagnied by all images. When an image is unreadable in your report and missing from your submission archive, you will not receive any points for that task. Make sure to mention the names and student IDs of both team members. The other team member must submit a single HTML file containing only the coordinates of both team members. You may use this template. This will allow us to put in grades for both team members in BlackBoard.
  • Submission Medium: BlackBoard Ultra. Beware that BlackBoard's clock may differ slightly from yours. If BlackBoard is not reachable due to an (unpredicted) maintenance, you submit your solution via e-mail to the TA. Make sure all group members are in CC!
  • Contact / TA: Randy Paredis.

Goals

In this assignment, you will use the Use Cases, UML Sequence Diagrams, Regular Expressions, and State Automata modelling languages to design and verify an the communication in a port. You will also make the link to an output trace an actual implementation in Python to perform the checking. At the end, you will be able to automatically determine, based on the obtained trace file, whether all requirements are satisfied or not. Figure 1 shows an overview of the parts in this assignment.



Figure 1: Main overview of the assignment.

Problem Statement

A ship's captain is not allowed to manouver the ship anywhere inside a port. This is because they do not know where the docks have been dredged and how to best manouver towards their destination quay. Instead, a (port) pilot (nl: loods) will steer the ship throughout the confines of the port. Typically, there are different kinds of pilots. For this assignment, we concern ourselves with an outside pilot (concerns themselves with helping the ships enter/exit the port; nl: buitenloods), an inside pilot (concerns themselves with navigating the docks; nl: binnenloods) and a lock pilot (concerns themselves with the navigation inside the locks; nl: sluisloods). Figure 2 gives a generic overview of the port we will be looking at.



Figure 2: The port to engineer for the assignment.

A ship is typically not allowed to enter a port immediately. Large vessels are required to wait outside of the port. In the figure, A denotes this waiting area and B the destination quay of the ship. The Harbour will act as a central control unit. In short, the behaviour of this port can be described as:

  • A ship arrives at A and communicates this to the Harbour.
  • The Harbour tries to dispatch an outside pilot from PBO (Pilot Building Outside). If no outside pilots are available, the ship will keep waiting.
  • The outside pilot will navigate the ship until node PO.
  • When the Harbour learns that the ship has reached PO, it will try to dispatch a lock pilot from PBL (Pilot Building Locks). If no lock pilot is available, the outside pilot will keep waiting on board of the ship. If a lock pilot is dispatched, the outside pilot returns to their station (PBO).
  • When the Harbour learns that a ship has arrived at G0 (Gate 0), it will request the Lock Controller to try and open this gate. The same logic applies to G1 (Gate 1) and G2 (Gate 2).
  • When the Harbour learns that a ship is inside the first lock (L0), it will request the Lock Controller to close G0. The same logic applies to L1 (Lock 1) and G1.
  • When the ship communicates it has reached node PI, an inside pilot will be requested from PBI (Pilot Building Inside). Furthermore, the Harbour requests to close G2. If no inside pilots are available, the ship keeps waiting, with the lock pilot on board. If an inside pilot is dispatched, the lock pilot returns to their station (PBL).
  • When the ship reaches their quay B, the inside pilot returns to their station (PBI).

You are given a simple implementation of this port that handles the arrival and movement of ships. It is your task to check whether or not the specified requirements are validated. However, you are only given access to trace files of the behaviour of this system (due to the exection of code). A trace file contains debugging information about the port, such as all ship positions, opening/closing of lock gates, and pilots that get dispatched. Due to this verbosity, and the total runtime of the execution, the file is quite long, and therefore validating the requirements is not to be done manually. Thus, the validation will be done automatically. You will first model a set of Regular Expressions, and then a set of Finite State Automata, which you will subsequently encode, to automatically verify whether the system implementation complies with the system specification given in the requirements below (and modelled visually in Sequence Diagram form).



Figure 3: The UML Class Diagram for the port.

The structure of the port is described in figure 3. Some additional information is provided below. You are allowed to ignore all time-based variables (i.e., all durations) in your solution.

  • Position: Enumeration that allows the identification of the current ship position.
  • Ship: Identification of a ship that wants to enter the port. Each ship has a unique ID. The waiting counter is used to identify how long a ship must remain idle. The finished boolean is set once the ship has reached node B.
    • tick(void): void This method will be called for each ship in the port, every iteration of the simulation. When the ship is not idle, it will signal its position to the Harbour.
    • advance(duration: int): void Moves the ship to the next position and requests an idle time for some duration. This behaviour mimics the time delay to move from one position to another.
    • arrived(void): void Called when the ship has reached its destination.
  • PilotBuilding: Represents a resource pool of pilots that can be dispatched. It has a name for unique identification and a certain amount of pilots, stored in the pilots field.
    • seize(duration: int): bool Requests a pilot from the building. If a pilot is available, the Harbour will be notified that they were dispatched. The duration identifies how long it takes for the pilot to reach and steer the ship. Returns whether or not it was possible to dispatch a pilot.
    • release(void): void Releases a pilot back to the resource pool. For the sake of simplicity, this happens instantaneous.
  • LockController: Handles the opening and closing of the locks. It has a gates list of booleans that identify the lock gates. The gate at index 0 represents G0, the one at index 1 is G1 and G2 is at index 2. When the boolean value is false, the gate is closed. When true, it is open.
    • open(lock_id: int): void Opens a specific lock if possible. See the requirements below for more info.
    • ship_at_lock(ship_id: int, lock_id: int): void Used by the Harbour to notify that a ship is at an open lock gate.
    • ship_past_gate(ship_id: int, lock_id: int): void Used by the Harbour to notify that a ship has sailed past a lock gate and closes this gate.
  • Harbour: Global controller of this system. Handles all communications. In the simulation, the Harbour first selects the current ship before the tick() method is called, resulting in a ship-by-ship handling of all logic.
    • pilot_dispatched(duration: int): void When called, it is known that a pilot was dispatched for the current ship.
    • ship_position(ship_id: int, pos: Position): void Called by the ship to notify the Harbour of its position. Depending on the current ship's position, other communication messages are being send.

This results in the following requirements:

  1. A ship must be created before it can move through the port.
  2. Each iteration, each ship must notify the Harbour of its position, unless the ship is in-between two positions.
  3. A ship must pass through all positions in the correct order, being: A, PO, G0, L0, G1, L1, G2, PI, B.
  4. When a ship is at an open gate, the gate must not close until the ship has passed the gate (i.e., the ship is at the node after the gate).
  5. A lock gate may only open if the previous and next gate (if it exists) are closed.
  6. A PilotBuilding should not dispatch a pilot if there are no pilots available.
  7. When a ship is waiting for a pilot, eventually a pilot will be dispatched.
  8. The amount of available pilots in a PilotBuilding must decrease after a dispatch and increase after a release.
For simplicity of this assignment, you will only need to check use case 4 and 5.

Note that the trace will only terminate as soon as all ships in the port have arrived at their destination. For example, if a ship arrives at A, the trace will always contain the arrival of the ship in B. Furthermore, each iteration, all ships will be handled in order. This means that if ship 0 gains a pilot, the dispatch will happen before ship 1 is handled. You can use this information to make some of the rules a little simpler.

Tasks

You will need to perform the following tasks step by step:

  1. Write full Use Cases using the use case template (for ONLY requirements 4 and 5).
  2. Design the dynamic interaction behaviour in UML Sequence Diagrams for the above use cases (ONLY requirements 4 and 5), using the textual rendering tool PlantUML, or using the online tool WebSequenceDiagrams. Start from the Class Diagram to know what objects and methods you can use. Describe all possible options. Use variable names to reduce complexity. Clearly indicate the pre- and postconditions for your Sequence Diagrams.
  3. Write Regular Expressions (RegEx) (refer to the format of the given output trace) for verifying the above use cases.
    To make life easier, we use abbreviations to shorten the messages that you need to recognize in your RegExp/FSA. Here are the mappings: 
                    SC x   := A ship is created with ID x
                SA x   := The ship with ID x has arrived at its destination
                SP x p := The ship with ID x is at position p
                SL x y := The ship with ID x is at open lock gate y

                LO y   := Lock gate y is now open
                LC y   := Lock gate y is now closed

                PD n x := Pilot building n has dispatched a pilot to the ship with ID x
                PR n x := Pilot building n has regained a pilot from the ship with ID x
    The following is a complete example regular expression to check use case 1: 
                    SP (\d+) .+\n(.|\n)*?SC \1\n
    An explanation of this regular expression is as follows: we try to find a ship position notification (SP), followed by a ship creation message (SC) of that exact ship. Where the ship is positioned is not important (.+). For the ship's ID, it is known that it is an integer, resulting in \d+. Because we want to refer to the same ship, we group the ship's ID and refer to it afterwards with \1.

    Whenever this RegEx matches, we know there is a violation of the requirements. This is called a negative match. A positive match does the opposite: the code is deemed correct if the trace matches your description (in Regular Expressions, FSA, ...). For all parts, you are allowed to use either a 'positive match' or 'negative match'. Do explain why you used either kind of match, and make sure to reply "correct" or "violation" in the end, instead of saying "matched" or "not matched". Choosing the right kind of match might significantly shorten your solution!

    Another, more complicated example (using a positive match) is the complete regular expression to check use case 7 (Note: this part has been edited!): 
                    Count the Amount of Ships Using:
                  (SC \d+\n)

                Outside Pilot Dispatching:
                  ((SP (\d+) A\n)((?!SP \3 A\n)(.|\n))*(PD PBO \3\n))

                Lock Pilot Dispatching:
                  ((SP (\d+) PO\n)((?!SP \3 PO\n)(.|\n))*(PD PBL \3\n))

                Inside Pilot Dispatching:
                  ((SP (\d+) PI\n)((?!SP \3 PI\n)(.|\n))*(PD PBI \3\n))
    An explanation for the ReGex of the outside pilot dispatching rule follows: first, the total amount of ships in the system is counted using the first RegEx. This identifies the total amount of matches that the other regexes require. For each of the other RegExes, you first find a ship at a pilot requesting position, for which we look for the last occurrence in the trace. This is followed by a dispatch of the correct pilot. This pattern must appear x times, where x is the amount of matches for the first RegEx. The same logic applies to the other two RegExes.

    As you want this to be correct for all pilot buildings, you need to run both of them seperately. If all of them find x mathces, the trace is as expected. However, if one of them doesn't match x, an error is found. You can check the validity of the above RegEx using an online tool like Regex101.

    Clarification: the above uses a Regular Expression notation commonly used in UNIX Regular Expressions (as used in the stream editor sed, for example). Below, you can find a short description of RegEx notation, as is required for the assignment.

    • [eE] stands for e or E.
    • [a-z] stands for one of the characters in the range a to z.
    • ^ means "match at the beginning of the trace".*
    • $ means "match at the end of the trace".*
    • X|Y means "match either X or Y", with X and Y both sub-expressions.
    • [^x] means not x, hence ^[^E].*\n matches every line except those that start with the E character.
    • . matches any single character. Depending on the used program, the . might either match a newline or not.* In Python's re module, this does not match a newline by default.
    • X? matches 0 or 1 repetitions of X.
    • X* matches 0 or more repetitions of X.
    • X+ matches 1 or more repetitions of X.
    • \ is used to escape meta-characters such as (. If you want to match the character (, you need the pattern \(.
    • The ( and ) meta-characters are used to memorize a match for later use. They can be used around arbitrarily complex patterns. For example ([0-9]+) matches any non-empty sequence of digits. The matched pattern is memorized and can be referred to later by using \1. Following matched bracketed patterns are referred to by \2, \3, etc. Note that you will need to encode powerful features such as this one by adding appropriate actions (side-effects) to your automaton encoding the regular expression. This can easily be done by storing a matched pattern in a variable and later referring to it again. It is, however, not required to implement this feature to be used anywhere. You may require storing the ship's ID in the automaton/RegExes. It is sufficient to allow this functionality
    You are welcome to use different variant notations (such as the one used in the Python Regular Expression module), as long as you explain your notation.
    * Some programs allow additional RegEx flags that change the behaviour of these symbols. You may use these flags in your solution if you clearly indicate this in your report.

  4. Design a FSA which encodes the Regular Expressions for verification (example). You can use GraphViz, PlantUML, Diagrams.net or FSM to design your automata (note that in FSM, it is not possible to mark an initial state, so just name it "init").
  5. Implement this FSA for verification in the provided code framework (see scanner.py; an example is included at the bottom of the file).
  6. There are 6 output traces available for you to test your code out: trace1.txt, trace2.txt, trace3.txt, trace4.txt, trace5.txt and trace6.txt. Run your FSA implementation (which in turn implements the Regular Expressions, which in turn encode the checking of interaction behaviour use cases which were modelled as Sequence Diagrams) on the given output traces to verify the specification.
  7. There is an intentional bug in the implementation (which is visible in some of the traces) that causes the system specification not to be satisfied. You need to figure out which requirement is being violated, and show how your FSA which checks this. Identify which of the traces show the violation and which ones don't. Also describe in your own words what the meaning is of this bug; for instance: the ship gets crushed by the lock gate.
  8. Write a report that explains your solution for this assigment. Include your models and discuss them. Make sure to mention all your hypotheses, assumptions and conclusions. See also the "submission information" at the top of this page.

Take pride in your work. Make sure your report and all models and images are clearly readable. Additionally, produce clean and (preferrably) well documented code. If a text-to-figure transformation (such as for GraphViz and PlantUML) causes your images to be difficult to read, also include the source files from which these were generated (*.gv and *.puml). You will not lose points for doing too much, but you will lose points if you do too little.

Practical Issues
Maintained by Hans Vangheluwe. Last Modified: 2023/05/08 02:53:18.