Formal Methods: Z Schema Notation for BuyIt System Functionality

This paper presents a Z schema notation for the BuyIt system, an online platform designed for product purchases and sales. The Z schemas are created to illustrate the input and output variables of the BuyIt system, focusing on non-functional requirements. The paper covers key functionalities, including user registration, sign-in with access control, product upload, product search, purchase processes, and user reputation management. It includes detailed schemas for each function, outlining preconditions and postconditions, and uses parameters like password, product, email, and reputation to define the system's operations. The system also includes a user punishment mechanism for users who violate the platform's policies. The paper emphasizes the importance of security and risk management in the system design and references related research papers.

Running Head: Z SCHEMA NOTATION FOR BUYIT SYSTEM 1
The Z Schema Notation for Buyit System
Institution
Date
Name

Z SCHEMA NOTATION FOR BUYIT SYSTEM 2
Contents
Introduction.................................................................................................................................................3
Z schemas....................................................................................................................................................3
Registration.................................................................................................................................................4
Sign In......................................................................................................................................................5
Upload Product........................................................................................................................................5
Product Search.........................................................................................................................................6
Purchase..................................................................................................................................................7
Reputation...............................................................................................................................................7
Punish User.............................................................................................................................................8
References...................................................................................................................................................9

Z SCHEMA NOTATION FOR BUYIT SYSTEM 3
Introduction
Powering businesses with latest online technologies is the future of many businesses in
these technological times. Almost all the manual business paperwork has been taken over by
technology. BuyIt is an online catalog where users are able to make product purchases or sell
products as well. This online software management system will allow a buyer to give their
destination address and they are prompted to make payments through their credit cards online
(Singh, Sharma & Saxena, 2016). After this, the item bought will be shipped to the desired
location of the buyer. This robust system, therefore, needs to have a good foundation with regard
to its security and risk management. BuyIt’s main goal is to increase business revenue collected
from the internet and to bring together the buyer and seller on a platform which keeps user
integrity and secure payment gateways. We have designed Z schemas representing various
operations of the BuyIt software in this paper (Khan & Jamshed, 2016).
Z schemas
Z schemas have been created in order to easily illustrate all the input and output variables
used by ButIt to accomplish all of its non-functional requirements (Singh, Sharma & Saxena,
2016). I order to complete all the actions, an array of functions were created. They are Register
user, login, and user reputation, upload new products, search product and punish user. The Z
schema below best illustrates all these functions.
Distinct parameters have been utilized by the schemas developed below. These parameters
have been noted to be the basic elements that are required for the smooth working of the BuyIt system.
Password: This parameter represents the security passcode which every user will give as input
so that they are authorized to use the BuyIt system.

Z SCHEMA NOTATION FOR BUYIT SYSTEM 4
Product: This represents the name of item that is available on the BuyIt portal and can be
viewed by other potential buyers.
Email: this is a unique identification parameter that needs to be used during registration. A user
will confirm their email before a successful sign up.
Reputation: this is a natural integer that represents the score level of a user. It will be updated
by the correspondent user every time a successful purchase is done.
Condition: This is the state of the product
Cost range: this is the range of the prices of items.
Init
Δ BuyIt
Hwm = 0
Registration
Register User
ΞRegister
Em? :EmailAddress
Passw? : UserPassword
User? :Username
Em? ∉ known
Email ∉ known
Passw′ = UserPassword ∪ {em?↦ Passw?}
The register user schema above shows the user inputs of email address and password.
These values will later be used for signing into the system. There are two pre-conditions in this
case. The email address and username provided by a user should not be known or not in the
database already. That is em?
∉ known and email ∉ known. The email and password will later
be associated together for that user and saved. i.e. passw′ = UserPassword
∪ {em?
↦ Passw?}

Z SCHEMA NOTATION FOR BUYIT SYSTEM 5
Sign In
Access control is a crucial component for all award winning software systems. This aims at protec
confidentiality and integrity of user information. BuyIt has implemented this by first ensuring that a user
authenticated before accessing its products and services. The user input i.e. email and password are encry
latest encryption technologies in order to ensure that data is always safe even when cybercriminals haze m
the primary database of the system (Yang & Jia, 2014). The password furthermore must be a strong passw
password is characterized to be a combination of lowercase and uppercase letters, numbers, characters, an
symbols.The user must provide his email and password during the signing in (Em? :EmailAddress
Passw? : UserPassword)
. The mail and password should match on the database in order for a sign in to become
successful. If the email and password no not match, the sign in session is regarded as failed.
Sign in
Em? :EmailAddress
Passw? : UserPassword
If em ∈ EmailAddress ∧ passw ∈ UserPassword ∧ userstat = Active
Then alert signin = success
Else alert signin = failed
Upload Product
Before a product is visible to potential buyers for purchase, it must be uploaded to
the BuyIt database. This schema has some preconditions which are: the product name can be
known or not known by the system, the cost of the product must not be left empty (cost? =
notnull), and the product specification also must be made (spec? = notnull).

Z SCHEMA NOTATION FOR BUYIT SYSTEM 6
Product Upload
ΔUpload
Product? :Nameofitem
Cond? :Conditionoftheitem
Cost? :costofitem
Loc? :Location
Spec? :ItemSpecifications
Product? ∈ known ∨ ∉ known
Cost? = notnull
Spec? = notnull
and
Product Search
In this schema of Product search, the predicates illustrate that there is an index i at which
the products array contains an input product? And the outputs cond! And spec! Are
corresponding elements of the array products. So that this happens, the product? Input needs to
appear at some place in the array products. This will become the pre-condition of the search
operation.
Item Search
Ξ FindIt
Product? :NameofItem
Cost_range? :Itemcostrange
Loc? :Itemlocation
Product? ∈ known
Cost_range? ∈ known
Loc? ∈ known
Cond! =Itemcondition
Spec! =itemspecifications
∃ I : 1 . . hwm ⦁ Product? = products (i) ∧ cond! = conditions (i) ∧spec! = specs(i)

Z SCHEMA NOTATION FOR BUYIT SYSTEM 7
Purchase
When purchasing an item, BuyIt provides for a user to check out and pay using their
credit card. Before payment, BuyIt will sum up the cost of the item (s) together with the cost of
shipping in order to give how much the buyer needs to pay. When making the payment, several
preconditions apply. The user’s credit card balance is not below the total cost of item bought and
the shipping location and quantity of items must be provided.
Purchasing an Item
Δ Purchase
Credit: ℕ Availablecreditcardbalance
Postage: ℕ Costofshipping
Item: ℕ Costofitem
Ship? :ShippingLocation
Cost_tot: ℕ totalcostofitem
Quant: ℕ quantityofitems
if userstatus =Active
∧ credit ≠ zero
∧ quant ≠ null
∧ ship? ≠ null
then cost_tot = item *quant + postage
credit = credit – cost_tot
else Alert “you have less cash in your credit card Please recharge to continue”
∨ “quantityofitems cannot be empty”
∨ “you must provide your ShippingLocation”
Reputation
A good management system needs to keep track on its users and punish users who
go against the policies set for the smooth running of the business (Madhan, Kalaiselvi & Donald,
2017). This strategy will greatly help reduce non-existent products. In that, any user that uploads
a product with description and all required options and then when a buyer wants the product, the
product won’t be delivered because it did not exist in the first place. In such a situation, the
purchaser will give a reputation score of less than one and the user will be blocked from

Z SCHEMA NOTATION FOR BUYIT SYSTEM 8
accessing the system and their non-existent products will be removed from the BuyIt portal. The
user reputation must be between 0 and 5. The previous reputation is averaged with any new
reputation score awarded to a user
Reputation
ΔReputation
User_reput? : ℕ ReputationoftheUser
Old_reput? :ℕ UserreputationfromPreviousTransactions
let user_reput? ≥ 0
user_reput? ≤ 5
If userstatus = Active
then (old_reput + User_reput) ÷ 2 = user_reput!
else userstatus ≠ Active
Punish User
When the reputation of a user falls below zero, they are not allowed to continue
using BuyIt services. The account is thus blocked this is a punishment so as to ensure that both
the buyer and seller successfully provide great products and keenly select the products they need
respectively (Fifield, Lan, Hynes, Wegmann, & Paxson, 2015). This, in the end, guarantees
efficient and professional transactions are achieved through the BuyIt portal.
PunnishLowReputationUsers
User_reput!
If user_reput < 1
then user_stat = blocked
else user_stat = active

Z SCHEMA NOTATION FOR BUYIT SYSTEM 9
References
Fifield, D., Lan, C., Hynes, R., Wegmann, P., & Paxson, V. (2015). Blocking-resistant
communication through domain fronting. Proceedings on Privacy Enhancing
Technologies, 2015(2), 46-64.
Khan, S. A., & Jamshed, H. (2016). Analysis of formal methods for specification of e-Commerce
applications. Mehran University Research Journal Of Engineering &
Technology, 35(1), 19.
Madhan, V., Kalaiselvi, V. K. G., & Donald, J. P. (2017, February). Tool development for
formalizing the requirement for the safety critical software engineering process.
In Computing and Communications Technologies (ICCCT), 2017 2nd International
Conference on (pp. 161-164). IEEE.
Singh, M., Sharma, A. K., & Saxena, R. (2016). An UML+ Z framework for validating and
verifying the Static aspect of Safety Critical System. Procedia Computer
Science, 85, 352-361.
Tan, W. K., & Teo, H. H. (2015, August). Productpedia–A Collaborative Electronic Product
Catalog for Ecommerce 3.0. In International Conference on HCI in Business (pp.
370-381). Springer, Cham.
Yang, K., & Jia, X. (2014). DAC-MACS: Effective data access control for multi-authority cloud
storage systems. In Security for Cloud Storage Systems (pp. 59-83). Springer, New
York, NY.