Requirements Checking Assignment 

Practical Information

  • Due Date: 22 October before 23:55.
  • 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. The report must be called index.html. Make sure to mention the names and student IDs of all the team members. The other team member must submit a single HTML file containing only the coordinates of both team members. This will allow us to put in grades for both team members in BlackBoard.
  • Submission Medium: BlackBoard. 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 automatic PRT junction controller. 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.

Problem Statement

A Personal Rapid Transit (PRT) is a small rail network over which trolleys (or rail carts) transport people. Typically, each rail cart only transports a limited (< 10) amount of people over a relatively short distance. Ensuring the transport of large amounts of people, a lot of trolleys travel over a railroad riddled with a vast amount of junctions. To minimize the human error in this trajectory, these junctions should be automated.

You are given an implementation of a simple junction controller, which needs to set the traffic lights of the segments coming in to the junction. It is your task to check whether or not the specified requirements are validated. However, you are only given access to a trace file of the execution. This trace file contains debugging information about the junction, such as all incoming signals, outgoing signals, and internal timers that get triggered. 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). The structure of the junction is described in the following UML Class Diagram:

The behaviour of the PRT junction can be described as follows:

  • By default, all traffic lights that prevent the entry to the junction are set to red for safety.
  • The railway segments continuously check for the presence of a trolley on that segment. As soon as a trolley is detected, a signal is sent to the controller.
  • The controller will process these incoming signals, and will put the traffic light of the requesting segment to green. This on the condition that there is currently no trolley on the junction itself, and that the traffic light on the other entry to the junction is red too.
  • As soon as a trolley has entered the junction, all traffic lights for entry to the junction are put to red again.
  • If it is detected that the junction is clear again, new (or queued) requests are handled.
  • For safety, the signal to the traffic light is sent out every second (such that traffic lights can detect if there is a problem with the connection).

This results in the following five requirements:

  1. If a trolley wants to enter the junction, it will eventually get a green light.
  2. If a trolley enters the junction, all traffic lights to the junction become red.
  3. If a trolley is on the junction, all traffic lights will remain red until that trolley has left the junction.
  4. If two trolley are waiting to enter the junction at the same time, permission will be granted in order of arrival (i.e., the first trolley to arrive will get a green light, and the second one has to wait).
  5. The controller will send the traffic light signals out every second.
For simplicity of this assignment, you will only need to check use case 3 and 4.

Note that the trace will not terminate while there are still trains on any of the tracks. That is, for every enter event, there will be an exit event in the trace. You can use this information to make some of the rules a little simpler. For example, if a trolley wants to enter the junction, the trace will only terminate when that trolley has left the junction.

Tasks

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

  1. Write full Use Cases using the use case template (for ONLY use cases 3 and 4).
  2. Design the dynamic interaction behaviour in UML Sequence Diagrams for the above use cases (ONLY use case 3 and 4), 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.
  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: 
                    E := A trolley enters the specified segment
                R := A red signal is sent to the specified segment
                G := A green signal is sent to the specified segment
                X := A trolley leaves the specified segment
    Beyond that, each segment has a simple encoding: 
                    1 := left incoming railway segment
                2 := right incoming railway segment
                3 := outgoing railway segment
    For example, "G 1" means that the left incoming railway segment got a green light. The following is a complete example regular expression for use case 1: 
                    Regular expression pattern for rule 1 (for segment 1):
                ^((([^E].*)|(E [23]))\n)*(E 1\n(.*\n)*G 1\n((([^E].*)|(E [23]))\n)*)*$

                For segment 2:
                ^((([^E].*)|(E [13]))\n)*(E 2\n(.*\n)*G 2\n((([^E].*)|(E [13]))\n)*)*$
    An explanation of rule 1 for segment 1 follows: we try to find an E 1, for which we can skip over everything that is not equal to E 1. As soon as E 1 is then found, we keep matching everything until we find a green light for segment 1. After that, we can match anything except for E 1 again. Note that "anything except for E 1" is encoded as (([^E].*)|(E [23]))\n.

    As you want this to be correct for both incoming segments, you need to run both of them seperately. If all of them match, then the output is as expected. However, if either of them doesn't match, 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).

    • [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 a line/string".
    • $ means "match at the end of the line/string".
    • 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 and use this feature, as long as you visually indicate corresponding patters.
    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.

  4. Design a FSA which encodes the Regular Expressions for verification (example). You can use GraphViz, PlantUML 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: two trains merge at the junction and form a single train.
  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.

For all parts, you are allowed to use either a 'positive match' or 'negative match'. With a positive match, the code is deemed correct if the trace matches your description (in Regular Expressions, FSA, ...). With a negative match, the code is deemed wrong if the trace matches your description. 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!

For example, you could check requirement 1 by checking that every E 1 and E 2 is met with an E 3, thus a positive match: if your Regular Expression matches, the requirement is satisfied. You could also check the requirement by matching a situation in which there is an E 1 without any E 3 after it, thus a negative match: if this regular expression matches, the requirement is not satisfied.

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: 2022/08/29 00:29:58.