CSCI910

Assignment 2

Group Assignment

Marks: 30

1. Objective

The objective of this project is to test your understanding and skills in using informal and formal specification approaches and models to represent the requirements for a software system. Assignment 2 builds upon the project description provided in Assignment 1. You are required to complete models using Finite State Machines (FSM), Coloured Petri Net (CPN) and Z Schema.

2. Problem Description

In this project, you are asked with modeling the procedures of the UOW Library Management System. The general process is outlined below. You can make reasonable assumptions where details are not specified.

2.1. User Registration

Customers and librarians can register their UOW library account through the UOW library’s homepage by providing a username, email address, and password. Additionally, the system allows users to select their user type. Customers should select the “Student” or “Uni Staff” option, and librarians should select the “Librarian” option. If the entered username already exists in the system, the email format is invalid, or the password has less than six characters, the registration page will show error messages. Once all inputs are valid, and the user clicks the “Sign Up” button, the user’s information will be sent back to the UOW server.

2.2. Login to the UOW Library System

Customers and librarians can log in to the UOW library account via the UOW library’s homepage by entering their username and password and clicking the “Login” button. The login information is sent back to the UOW server for authorization. Upon successful authentication, the customer/librarian account information is displayed, allowing them to access the UOW library service. Otherwise, the customer/librarian will be asked to re-enter username and password. Invalid login attempts over three times trigger a confirmation email to reset the password.

2.3. View and Search Books

After successfully logging into the UOW library system, customers can search for books using various criteria such as title, keywords, author names, categories, etc. If the customers want to know details about a particular book, they can click the book’s link, and a new page will show the book details, including book title, author name, book abstract, PDF link, and the borrow link.

2.4. Borrowing and Returning Books

After customers click the borrow link, the page will show the book availability and location within the UOW library. If the book is available, the customer can click the “Borrow” button. Then the page will show the borrow  information and the latest return date, and the borrowing information will show in the borrowing history. When  customers want to return books, they can click the “Return” button, and the page will show all borrowed books  by this customer. Customers can select the book they want to return by clicking the book name. If the date is  before the latest return date, the return process will be completed immediately. If the date is after the latest return  date, then customers need to pay the penalty fee. The page will show the penalty costs, and the customer needs to  fill in the credit card information. After the customers enter all required information, they can click the “Confirm” button to complete the payment.

2.5. View Borrowing History

The customers can view all historical borrowing records by clicking the “View” button on the home page. The customer can also search a particular historical record based on the book title. Once the customer finds the record, by clicking the record’s link, a new page will show the borrowing information, including the borrowing date, returning date, book information, etc.

2.6. Booking Library Space

After the customers log into the UOW library system, they can book library rooms for study. On the UOW library home page, the customer can click the “Book a Room” button, and then the page will show the room information and time slots with different colors. Green time slots are available, red time slots are unavailable or padding, and yellow time slots are booked by the customer. When the customer selects green time slots and clicks the “Submit Times” button, the page will be redirected to the confirmation page, which shows the username, email address, library room number, and selected time slots. The customer can click the “Submit My Booking” button to confirm.

2.7. Catalog Management

The catalog management page provides librarians with the functionality to add, update, and remove books from the catalog through three buttons, i.e., “Add”, “Update”, and “Remove” . Clicking the “Add” button redirects librarians to a new page, enabling the input of essential book details like title, author, ISBN, and publication date. Clicking the “Update” button prompts librarians to use a search function, helping them locate the specific book in the catalog. Once the book is found, librarians can select the corresponding book name to view and edit its details. Librarians can click on the “Edit” button to enter the editing mode and modify the title, author, ISBN, and publication date. After making the necessary updates, librarians click the “Save” button to save changes. Also, the “Remove” button allows the librarians to use search functionality to locate the book. Once the book shows on the page, librarians select it and click the “Remove” button again to remove the book.

2.8. Logout the Library Management System

The customers and librarians can log out of the UOW library system anytime by clicking the “Logout” button. If the customer/librarian does not have any action over 30 minutes, the account will be logged out automatically. After the customer/librarian logs out, the browser will jump to the home page.

2.9. System Requirements

The UOW library system shall be available 24 hours per day and 7 days per week. The system shall support up to 100,000 people to use concurrently, and the system delay shall be no more than 10 seconds. If a customer/librarian disconnects from the system accidentally, the system will automatically log out. If the library system is down, a backup  system  shall be  activated and take over the original  system automatically. This procedure  shall be completed within 60 minutes.

3. Tasks

This project contains three tasks.

3.1 Design and draw a Finite State Machine (FSM) for the ‘User Registration ’ and the ‘Login/logout UOW Library System ’ to clearly show the different states of the user registration and the user login/logout, such as new registration, username already existence, successful login, wrong username and password, reset password, and successful logout, and the events changing the  states. You shall also complete the state transition table associated with your FSM. The state name and event name must be meaningful. (10 marks)

3.2 Design and create a Colored Petri Net to show the common behaviours of library customers in using the UOW library system, i.e., registration, login/logout, search a book, borrow a copy of a book, and return a copy of a book (no need to consider the penalty fee). You shall define the Colored Petri Net with the mathematical representation and graphic representation, i.e., clearly specify the content of C = (P, T, I, O), the initial marking μ, and defines all color sets. Your proposed CPN shall be able to simulate the scenarios that multiple customers use the UOW library system and work on different tasks concurrently, such as registration, login, borrow/return a book. You can have reasonable assumptions of the scenarios in your simulation. (10 marks)

3.3 Complete Z  Schemas for the ‘Catalog Management ’ operations, i.e., the add operation, the  search operation, the edit operation, and the remove operation. Each operation shall cover both successful and unsuccessful scenarios. Your schemas shall also include the necessary definitions, such as the data types, the axiomatic descriptions, the system state schema, the initialization schema and the full operation schemas. (10 marks)

4. Submission

Students must submit solutions to Moodle Assignment 2. Email submissions will NOT be accepted.

4.1. For the FSM, you can draw it using Microsoft word or other professional tools. Finally, you shall create a pdf file (named fsm.pdf) to include everything about your finite state machine.

4.2. For the Colored Petri Net, you must create a pdf file (named cpn.pdf) to include the mathematic representation, the graphic representation and other necessary information about your CPN. CPN Tools (or CPNIDE) MUST  be used for the implementation. Please also submit your cpn file.

4.3. For the Z schemas, you must draw them using the z-editor (https://z-editor.github.io/) or other professional tools and create a pdf file (named schemas.pdf) to include all your schemas.

4.4. Please note, hand drawing of any diagram will receive a Zero mark for that task. Assignment 2 is a group work, only one member make your group submission to the Moodle. Please just submit a zipped file to include all required files, i.e., fsm.pdf, cpn.pdf, schemas.pdf and the cpn file. Plagiarism will result a Zero mark, and all involved students will receive the same penalty.