Skip to content

Latest commit

 

History

History
315 lines (245 loc) · 7.77 KB

0003-analisys.md

File metadata and controls

315 lines (245 loc) · 7.77 KB

2. Analysis

Date: 2024-08-13

Status

Accepted

Context

Explore the problem

Consider a book store in a shopping mall. The customer selects the books from racks to purchase and put them into a shopping Cart. The customer brings the Cart with the selected books to cashier. The cashier scans each item with checkout system to prepare an order. The cashier requests to customer for payment. The customer gives credit card to cashier. The verifier and checkout system scans the card. The verifier accepts the card and payment is accepted. Customer signs the credit card slip. The purchased books are handed over to customer.

Scenarios and User Stories documentation

In this point we express the needs that the user have in a form of user stories. It specifies the outcome that the user need

1. User Login

---
title: User Login Flow
---
flowchart LR
    A(Login) --> B{Valid?}
    B --> |No| A
    B --> |Yes| C(User Books Selection Flow)
Loading
Feature: User Login
  As a user
  I want to be able to log in with valid credentials
  So that I can access the system

Scenario: Valid login
  Given I have provided valid username and password
  When I submit the login form
  Then I should see the Books Selection Flow page

Scenario: Invalid login
  Given I have provided invalid username or password
  When I submit the login form
  Then I should be prompted to re-enter my credentials
  And I will not see the Books Selection Flow page

2. User Books Selection Flow

---
title: Books Selection Flow
---
flowchart LR
    A(User Logged) --> B{Empty Cart?}
    B --> |Yes| C(Search for books)
    C(Search for books) --> D(Add To Cart)
    D --> E{Finish?}
    B --> |No| E
    E --> |No| C
    E --> |Yes| F(Payment Generation Flow)
Loading
Feature: Search for books when cart is empty

Scenario:
Given I am a logged-in user
And my cart is empty
When I search for books
Then I should see a list of relevant books
Feature: Add book to cart when cart is empty

Scenario:
Given I am a logged-in user
And my cart is empty
When I add a book to my cart
Then the book should be added to my cart
Feature: Finish adding books to cart

Scenario:
Given I am a logged-in user
And my cart has books in it
When I finish adding books to my cart
Then I should see an option to proceed with payment
Feature: Proceed with payment when cart is not empty

Scenario:
Given I am a logged-in user
And my cart has books in it
When I proceed with payment
Then the payment generation flow should start
Feature: Search for books when cart is empty or not empty

Scenario:
Given I am a logged-in user
And my cart is empty or not empty
When I start searching for books
Then I should see a list of relevant books

3. Payment Generation Flow

---
title: Payment Generation Flow
---
flowchart LR
    A(User Cart) --> B(Process Order)
    B --> C(Customer Payment)
    C --> D(External System Payment Service)
    D --> E(Payment Confirmation?)
    E --> |No| C
    E --> |Yes| F(Payment Approved)    
    F --> G(Process Accepted Payment Flow)
Loading
Feature: Submit payment

Scenario:
Given I am a logged-in user with books in my cart
When I submit my payment information
Then the system should process my order
Feature: Process Order

Scenario:
Given I am a logged-in user with books in my cart
When I submit my payment information
Then the system should process my order and validate my payment information
Feature: Validate Payment Information

Scenario:
Given I am a logged-in user with books in my cart
When I submit my payment information
Then the system should validate my payment information and display a confirmation message if valid
Feature: Process Accepted Payment

Scenario:
Given I am a logged-in user with books in my cart
And my payment information has been validated as valid
When I submit my payment information
Then the system should process my accepted payment and display a confirmation message

4. Process Accepted Payment Flow

---
title: Process Accepted Payment Flow
---
flowchart LR
    A(Accepted Payment) --> G(Log Transaction)
    G --> F(Assemble Order)
    F --> E(Customer Receives shipping notice)
    E --> I(Invoice Creation)
    I --> J(Customer Receives Invoice)
Loading
Feature: Log Transaction

Scenario:
Given I have submitted my payment information and it has been approved
When the system logs my transaction
Then the transaction should be recorded and confirmed in the database
Feature: Assemble Order

Scenario:
Given I have logged my payment transaction successfully
When the system assembles my order
Then the system should confirm that all items in my cart are included in my order
Feature: Customer Receives Shipping Notice

Scenario:
Given I have assembled my order successfully
When the system generates and sends me a shipping notice
Then I should receive a notification with details about my shipment
Feature: Create Invoice

Scenario:
Given I have assembled my order and shipped it successfully
When the system generates an invoice for my order
Then the invoice should be created with accurate details about my purchase
Feature: Receive Invoice

Scenario:
Given I have assembled my order and shipped it successfully
When the system generates and sends me an invoice
Then I should receive an accurate invoice with details about my purchase

Formal Verification

Acceptance Criteria

We will use Payment Generation Flow with the following acceptance criteria

---
title: Payment Generation Flow
---
flowchart LR
    A(User Cart) --> B(Process Order)
    B --> C(Customer Payment)
    C --> D(External System Payment Service)
    D --> E(Payment Confirmation?)
    E --> |No| C
    E --> |Yes| F(Payment Approved)    
    F --> G(Process Accepted Payment Flow)
Loading
---
title: External System Payment Service
---
flowchart LR
    A(System) --> |External| B(Card Service)
    B --> C{Data Verification}
    C --> |Yes| D(Payment)
    C --> |No| J(Data verification Fail)
    J --> R(Response)
    D --> |External| E(Bank Service?)
    E --> F{Available Funds?}
    F --> |Yes| G(Debit)
    G --> H(Payment Confirm)
    H --> R
    F --> |No| I(Payment Rejected)
    I --> R
    R --> A

Loading
  • Architecture diagram for External api
---
title: Architecture diagram interaction for payment flow
---
architecture-beta
    group api1(cloud)[Local]
      service db(server)[System] in api1
    group api2(cloud)[External]
      service visa(internet)[Card Service] in api2
      service bank(internet)[Bank Service] in api2
      service bank_db(database)[Bank Database] in api2
    db:R --> L:visa
    visa:R --> L:bank
    bank:B -- T:bank_db
Loading

P Language model checker

Specifications

check clientserver PSpec

Executable Specification

check PTst

Quint model checker

Decision

Consequences

What becomes easier or more difficult to do, and any risks introduced by the change that will need to be mitigated.