The University of Melbourne
School of Computing and Information Systems SWEN90004 Modelling Complex Software Systems
Assignment 1b, 2021
Released: Monday 29 March. Deadline: 11:59pm, Sunday 19 April.
Ob jective
To use a higher-level modelling language to specify and reason about a concurrent system.
Background and context
Assignment 1 has two parts. The first part, 1a, was worth 10% of your final mark; this part, 1b, is also worth 10%. In the first part (which you should complete before attempting this part) you designed and implemented (in Java) a simulation of King Arthur and the Knights of the Round Table. Now the task is to model the system in FSP, use LTSA to check it, and to identify and mitigate any problems that you discover through modelling.
The tasks
There are three documents to submit and five sub-tasks to do. Remember to include your name on each submitted document.
First, model and check each of the two solutions you submitted in Assignment 1a. For each solution:
• Model: Model your Java implementation in FSP. That is, reverse engineer a FSP model from the Java code. Try to capture the essential interactions between the components— no more than that. The models should contain comments that explain the design and its components.
• Check: Specify what you believe are the relevant safety and liveness properties for your FSP model. Use LTSA to check these properties.
When these four sub-tasks have been completed, reflect on the experience, keeping your discus- sion to 400 words or less:
• Discussion: Which problems did you find in the two models as a result of using LTSA? Were these problems also present in the Java implementation? If you find problems with the Java solution submitted for part 1a, Solution 2, why do you think you picked these up now and not before submitting the Java code? If you did not find problems with your part 1a, Solution 2 submission, were you convinced when you submitted part 1a, Solution 2 that no problems existed? Why did you believe this? Do you still believe there are no problems?
Procedure and assessment
The assignment should be completed by students individually. A late submission will attract a penalty of 1 mark for every calendar day it is late. If you have a reason that you require an extension, email Nic well before the due date to discuss this.
To tackle the assignment, first work through (and understand) the examples from lectures, and do the workshop exercises. FSP is not difficult—it is simpler than most programming languages, and much simpler than a language like Java. However, as with other languages, the way to master it is to use it, and to learn by doing. Trying to do the assignment straight up may mean you struggle. Work through some easier examples first.
Submit a single zip file via the LMS. The file should include
• A file called sol1.lts with an FSP model for part 1a, Solution 1, including the relevant safety and liveness properties.
• A file called sol2.lts with an FSP model for part 1a, Solution 2, including the relevant safety and liveness properties.
• A file called discussion.txt, containing the discussion of issues. Please ensure that this is a plain text file; ie, not a doc, docx, rtf, or other file type that requires specific software to read.
All model files and your text file should contain, near the top of the file, your name and student number.
We encourage the use of the LMS’s discussion board for discussions about the project. However, all submitted work is to be your own individual work.
This project counts for 10 of the 50 marks allocated to project work in this subject. Marks will be awarded according to the following guidelines:
Criterion
Clarity, abstraction
Completeness
Correctness
Formatting
Discussion Total
Description Marks
FSP models are at a suitable level of abstraction. All be- haviours relevant to interaction are specified, and there is sufficient detail to implement the system from the model. Descriptions of all actions and processes are clear and con- cise.
The model is complete. All components have been modelled and all expected behaviour is present. Suitable safety and liveness properties have been described.
The original model accurately reflects the original imple- mentation (or specification). The modified model behaves “correctly” (ie, is free of problems identified in the original model), does not violate any safety properties, and demon- strates all liveness properties.
The FSP source adheres to the code format rules from Part 1a where this makes sense, including the use of comments to document model components and properties.
The discussion demonstrates understanding of the subject material.
2 marks
2 marks
3 marks
1 marks
2 marks 10 marks
Nic Geard March 2021
Why backwards?
A valid question: Why are we modelling the system after implementing it? Should it not be done the other way? Well, yes and no. Many people use modelling to understand an existing code base (just look at the number of tools for reverse engineering UML models from code bases). Reverse engineering is a great way to understand problems with an existing system; for example, why a deadlock is occurring. It is true, however, that in most cases, it would be cheaper and easier to do the modelling first.
The other reason why the assignment is “backwards” is that trying to model a new system using a new type of notation, such as FSP, will often end in disaster. We hope that, having gone through the Java programming stage, you feel familiar with the system to be modelled and thus can concentrate on the use of FSP. The exercise should be one of applying abstraction—a skill that is of utmost importance in any engineering discipline.
27