Itech7410 Software Engineering Methodologies | Z notation

Running head: ITECH7410 SOFTWARE ENGINEERING METHODOLOGIES
ITECH7410 Software Engineering Methodologies
Name of the Student
Name of the University
Author’s Note

1ITECH7410 SOFTWARE ENGINEERING METHODOLOGIES
Abstract
For the development of the Z scheme was to complete the task on time by organizing the task.
For the completion of the task it was divided into sub parts and time was allocated for
completion of each of the task.
A formal specification is prepared for a library management system with the application of Z
schema. The writing part of Z notation and explanation of predicate is done by student1 and the
other part like derivation of functionality is done by student2.
The task is based on library management system and for the development of the Z schema the
functionality of the system is analyzed. The Z notation is used as a formal technique for
improving the accuracy of the execution of the functionality and utilization of formal strategies
for the development of the programming framework.

2ITECH7410 SOFTWARE ENGINEERING METHODOLOGIES
Table of Contents
Functionality....................................................................................................................................3
Demonstration of the System.........................................................................................................10
Annotation of Z statement for the schema.....................................................................................14
Non-trival predicate statement.......................................................................................................17
Bibliography..................................................................................................................................19

3ITECH7410 SOFTWARE ENGINEERING METHODOLOGIES
Functionality
Add a book
LibrarySystem
name? : BOOK
rep! : MESSAGE
----------------------------
name? 6∈book
book ′ = book ∪ {name?}
directory ′ = directory
rep! = ‘OK’
If book exists
BookExists
ΞLibrarySystem
name? : Book
rep! : MESSAGE
---------------------------
name? ∈ book
rep! = ‘Book already exists’

4ITECH7410 SOFTWARE ENGINEERING METHODOLOGIES
Add a borrower
AddBorrowerOK
LibrarySystem
name? : Borrower
b?:BOOK
number ? : PHONE
-----------------------------
rep! : MESSAGE
name? ∈ borrower
name? number ? 6∈directory
directory ′ = directory ∪ {name? number ?} borrower ′ =borrower
rep! = ‘DONE’
Delete a book
RemoveBook
LibrarySystem
name? : BOOK
rep! : MESSAGE
---------------------------

5ITECH7410 SOFTWARE ENGINEERING METHODOLOGIES
name? ∈ book
book ′ = book \ {name?}
directory ′ = {name?} −⊳ directory
rep! = ‘OK’
Delete a borrower
RemoveBorrower
LibrarySystem
name? : BORROWER
rep! : MESSAGE
-----------------------------
name?
∈ borrower
borrower ′ = borrower \ {name?}
directory ′ = {name?} −
⊳ directory
rep! = ‘OK’
Return a book from a borrower
RetunBookOK
availablebook, availablebook′ : B BOOK
borrowedbook , borrowedbook′ : BOOK 7→USERNAME

6ITECH7410 SOFTWARE ENGINEERING METHODOLOGIES
--------------------------------------------------------------------------------
availablebook ∪ dom borrowedbook = BOOK
availablebook ∩ dom borrowedbook = ∅
availablebook′ ∪ dom borrowedbook ′ = BOOK
availablebook′ ∩ dom borrowedbook ′ = ∅
Ξ LibrarySystem Ξ LibrarySystem=b
[LibrarySystem | borrowedbook ′ = borrowedbook ∧ availablebook′ = availablebook
Enquire about a book
FindBooksOk
Ξ LibrarySystem
names! : B BOOK
rep! : MESSAGEAPP
----------------------------------------------------
number ?
∈ ran directoryname
names! = directory name−1 (| {number ?} |)
rep! = ‘DONE’
Reserve a book
LibrarySystem

7ITECH7410 SOFTWARE ENGINEERING METHODOLOGIES
b? : BOOK
------------------------------
B? 6∈Books
books′ = books ∪ {b?}
Enquire about a reservation
EnquiryBookReservation
ΞLibrarySystem
names! : B BOOK
r!:ReserveBook
rep! : MESSAGEAPP
---------------------------------------------
number ? ∈ ran directory
names! = directory −1 (| {number ?} |)
rep! = ‘DONE’
Cancel a reservation
CancelReserveBook
LibrarySystem
b? : BOOK

8ITECH7410 SOFTWARE ENGINEERING METHODOLOGIES
------------------------------------------
B? 6∈Books
books′ = books
∪ {b?}
names! = directory −1 (| {number ?} |)
rep! = ‘OK’
Buy a book
BuyBookOK
LibrarySystem
u? : USERNAME
b? : BOOKNAME
rep! : MESSAGEAPP
------------------------------------------------
b?
∈ availablebook
availablebook′ = availablebook \ {b?}
rep! = ‘DONE’
Receive a book
RecBookOK
LibrarySystem

9ITECH7410 SOFTWARE ENGINEERING METHODOLOGIES
u? : USERNAME
b? : BOOKNAME
rep! : MESSAGEAPP
----------------------------------------------------------------
b? ∈ availablebook
availablebook′ = availablebook \ {b?}
borrowedbook ′ = borrowedbook ∪ {b? u?}
rep! = ‘DONE’
Report of books on loan
RecBookOK
LibrarySystem
u? : USERNAME
b? : BOOKNAME
rep! : MESSAGEAPP
---------------------------------------------------------
b? ∈ availablebook
availablebook′ = availablebook \ {b?}
borrowedbook ′ = borrowedbook ∪ {b? u?}

10ITECH7410 SOFTWARE ENGINEERING METHODOLOGIES
rep! = ‘DONE’
Demonstration of the System
Add books
Add a borrower
Delete a book

11ITECH7410 SOFTWARE ENGINEERING METHODOLOGIES
Delete a borrower
Lend a book to a borrower
Return a book from a borrower

12ITECH7410 SOFTWARE ENGINEERING METHODOLOGIES
Enquire about a book
Reserve a book
Enquire about a reservation

13ITECH7410 SOFTWARE ENGINEERING METHODOLOGIES
Cancel a reservation
Buy a Book

14ITECH7410 SOFTWARE ENGINEERING METHODOLOGIES
Receive a Book
Report of Books on Loan
Annotation of Z statement for the schema
MESSEGES ::= OK | New Book Added| Not Added
─┌ Book
known: Name mgchgcjjℙ
Known : IDℙ

15ITECH7410 SOFTWARE ENGINEERING METHODOLOGIES
known : ? price
known : pages
└
┌ Borrower{ Name}? ID
└
MESSEGES ::= OK | Book Deleted| Not Deleted
─┌ Book
known : Nameℙ
known : IDℙ
known : ? price
known : pages
└
MESSEGES ::= OK | Borrower Deleted| Not Deleted
┌ Borrower
{ Name}
? ID
└
┌

16ITECH7410 SOFTWARE ENGINEERING METHODOLOGIES
lend Book Borrower
known : IDℙ
known : ? Price
{Name}
? ID
└
─
Message ::= Enquiry Ok | Not Start
└
┌ Enquiry Form
| known : Nameℙ
known : IDℙ
known : ? price
known : pages
{ Name}
? ID
└
─

17ITECH7410 SOFTWARE ENGINEERING METHODOLOGIES
Message ::= Done | Not Done
└
┌ Reservation
| known : Book Nameℙ
known : Book IDℙ
known : ? price
known : pages
{ Name}
? ID
└
Non-trival predicate statement
The statements can be predicted and it may be true or false. Some of the no trival
predicate statements are described that have relation with Library database system.
The True statements are given below:
Return =b ReturnOK ∨ InvalidReturn
For getting information about the borrowed books under the Library System and it is needed to
be checked that it is available or not.
ΞLibrarySystem =b
[ LibrarySystem | borrowed ′ = borrowed ∧ available′ = available′]

18ITECH7410 SOFTWARE ENGINEERING METHODOLOGIES
The next predicate is used for checking the name of book if it is in the database or not and also
giving a message if the name is invalid
FindBooks=b FindBooksOK ∨NotBook ∨InvalidName
There are some not predicate statement that may be an element of a specific set but not contain
any specific value. The values can be predicted and changes with any term.

19ITECH7410 SOFTWARE ENGINEERING METHODOLOGIES
Bibliography
Arcaini, P., Bonfanti, S., Gargantini, A., Mashkoor, A., & Riccobene, E. (2018). Integrating
formal methods into medical software development: The ASM approach. Science of
Computer Programming, 158, 148-167.
Chawla, S., Srivastava, S., & Bedi, P. (2017). Improving the quality of web applications with
web specific goal driven requirements engineering. International Journal of System
Assurance Engineering and Management, 8(1), 65-77.
Chohan, A. Z., Bibi, A., & Motla, Y. H. (2017, December). Optimized software product line
architecture and feature modeling in improvement of SPL. In 2017 International
Conference on Frontiers of Information Technology (FIT) (pp. 167-172). IEEE.
El Miloudi, K., & Ettouhami, A. (2018). A Multiview Formal Model of Use Case Diagrams
Using Z Notation: Towards Improving Functional Requirements Quality. Journal of
Engineering, 2018.
Grant, E. S., & Ajjimaporn, P. (2018). Pedagogical Benefits from an Exercise in Reverse
Engineering for an Aviation Software Systems. In CSEDU (2) (pp. 179-188).
Liu, Z., & Zhang, Z. (Eds.). (2016). Engineering Trustworthy Software Systems: First
International School, SETSS 2014, Chongqing, China, September 8-13, 2014. Tutorial
Lectures(Vol. 9506). Springer.
Singh, M., Sharma, A. K., & Saxena, R. (2016). Formal Transformation of UML Diagram: Use
Case, Class, Sequence Diagram with Z Notation for Representing the Static and Dynamic

20ITECH7410 SOFTWARE ENGINEERING METHODOLOGIES
Perspectives of System. In Proceedings of International Conference on ICT for
Sustainable Development(pp. 25-38). Springer, Singapore.
Weyns, D. (2017). Software engineering of self-adaptive systems: an organised tour and future
challenges. Chapter in Handbook of Software Engineering.