FORMAL METHODS – LECTURE 01 (COMPLETE DETAILED NOTES)

RELIABILITY

Reliability refers to the ability of a system to perform its required functions correctly
and consistently without failure over time.

In the lecture, the concept is raised with questions like:

• What is reliability?
• How important is it in our daily life?

This highlights that reliability is not just a theoretical idea, but a practical necessity.

In everyday life, reliability is extremely important in systems such as:

• Banking systems (e.g., ATM transactions must be correct)

• Air traffic control systems (errors can risk human lives)
• Medical systems (incorrect results can be dangerous)

A reliable system ensures:

• Correct output
• Consistent performance
• Minimal errors or failures

Therefore, ensuring reliability is one of the main goals of software engineering, and
formal methods help achieve this.

FORMAL METHODS

📌 Definition (from Encyclopedia of Software Engineering)

Formal methods are:

Mathematically based techniques used in developing computer systems for describing

system properties.

These methods provide frameworks that allow developers to:

• Specify systems
• Develop systems
• Verify systems
All of this is done in a systematic way rather than an ad hoc (random) manner.

📌 Another Definition

A Formal Method describes how to work with a language, meaning:

• Performing activities on its elements

• In order to achieve specific results

📌 Explanation from Lecture

Formal methods involve the use of:

• Logic
• Discrete Mathematics

These are applied in:

• Specification
• Design
• Development of software systems

🔷 COMPONENTS OF FORMAL METHODS

Formal methods mainly include:

• Formal Specification
• Theorem Proving
• Model Checking

Each of these helps in ensuring system correctness in different ways.

WHAT IS SPECIFICATION?

📌 Definition

A specification is:

An exact statement of the need to be satisfied or essential characteristics that a

customer requires and which a vendor must deliver.
📌 Software Specification

A software specification is:

A precise, unambiguous, and complete statement of the requirements of a system.

It is written in such a way that:

• It can predict how the system will behave

📌 Key Concept

Specifications define:
What a system should do

They do NOT define:

How the system will do it

FORMAL SPECIFICATION LANGUAGES

Formal specifications are written using:

• Mathematical notation
• Clearly defined:
o Vocabulary
o Syntax
o Semantics (meaning/interpretation)

🔷 APPROACHES
🔹 Algebraic Approach

In this approach:

• The system is described in terms of operations

• And the relationships between those operations

🔹 Model-Based Approach

In this approach:
 • The system is described using a state model
• Built using mathematical constructs such as:
o Sets
o Sequences

APPLICATIONS OF FORMAL METHODS

Formal methods are used in real-world systems where accuracy and correctness are
critical.

Examples from lecture:

• Paris metro line for traffic systems

• IBM’s Customer Information and Control System (CICS)
• Civil aviation display information system (UK air traffic management)
• Tektronix oscilloscopes
• Clinical neutron medical system (Washington)

These systems require high reliability, so formal methods are applied.

WHY SPECIFY FORMALLY?

Problem specifications (SRS) are essential for many purposes:

• Designing the system

• Validating the system
• Documenting requirements
• Communicating between stakeholders
• Reengineering systems
• Reusing solutions

Formal methods improve this process by:

• Producing higher-quality specifications

• Providing automated support

SPECIFY FOR WHOM?

Specifications are created for different types of users, including:

• Clients
• Domain experts
 • End users
• Architects
• Programmers
• Tools

Each of these has:

• Different backgrounds
• Different abstraction levels
• Different languages

Therefore, specifications must be clear and precise.

WHY USE FORMAL METHODS?

Formal methods provide several important advantages:

• They force developers to think systematically about problems

• They lead to better system design
• They allow early detection of inconsistencies and flaws
• They provide a precise reference for checking whether requirements are
satisfied (conformance)
• They help guide later development phases
• They serve as proper documentation within a development team
• They support reuse through specification matching

PRINCIPLES OF FORMAL METHODS

Formal methods are not just pure mathematics; they are focused on engineering
applications.

Key principles include:

• Formal methods require tools to be effective

• They emphasize understanding the difference between modelling and
programming
• Complexity is managed using abstraction
• Arguments are reduced to calculations that can be checked mechanically
• Manual reviews can be replaced by repeatable analysis
• They can be applied at different levels of rigor

Important statement from lecture:

Formal methods are part of practical systems engineering, not just theoretical
computer science.
 FORMAL MODEL STEPS

Formal modelling involves three main steps:

🔹 1. MODEL ABSTRACTION

Abstraction means:

Omitting details that are not relevant to the purpose of the model.

Important points:

• Not all real-world details are included

• Only important aspects are modeled
• Choosing what to omit requires engineering skill
• Usability of the modelling language is important

Example:

• Automata

🔹 2. MODEL VALIDATION

The aim of validation is:

To provide evidence that the model satisfies given properties.

In a model-based approach:

• Informal properties can be converted into:

o Processes
o Logical formulas

📌 Example from lecture:

Statement:
Clouds cause rain

Formal form:
Cloud(x) → Rain(y)
🔹 VALIDATION TECHNIQUES

Different techniques used in software systems:

1. Inspection
o Experts examine the model
2. Static Analysis
o Automatic checking of syntax and type correctness
o Detects unusual features
3. Testing
o Running the model and checking outputs
4. Model Checking
o Searching all possible states to find violations
5. Proof
o Using logic to reason about all possible states

🔹 3. MODEL REFINEMENT AND VERIFICATION

Refinement:

Transforming an abstract model into a more concrete (detailed) one

Verification:

Providing a formal argument that both models correspond correctly

Important points:

• As models become more detailed, verification becomes harder

• Tools are required to perform verification

COSTS OF FORMAL METHODS

• Increased development cost

• Requires skilled professionals
• Time-consuming process

BENEFITS OF FORMAL METHODS

• Improves system reliability

 • Detects errors early
• Produces high-quality software
• Provides strong verification

IMPORTANT STATEMENTS FROM LECTURE

• Formal methods are based on mathematical models

• They are difficult to apply but give fruitful results
• They do not mean programming a system
• They are used to verify system correctness using formal specifications

FORMAL METHODS – LECTURE 02

LOGIC AND FORMAL MODELS (THEORETICAL NOTES ONLY)

LOGICAL REASONING

📌 Definition

Logical reasoning is:

The systematic process of using structured thinking, rules, and evidence to analyze
information, solve problems, and derive valid conclusions.

📌 Explanation

Logical reasoning means thinking in a clear, organized, and step-by-step manner. It

involves:

• Using proper rules

• Analyzing given information
• Drawing correct conclusions

It helps in solving problems in a logical and valid way instead of guessing.

📌 Importance in Programming

Logical reasoning is very important because:

• Every computer programmer uses logic while writing code

 • Programs are based on conditions and decision-making
• Without logical reasoning, software cannot behave correctly

Therefore, a strong understanding of logical reasoning is essential for building

reliable software systems.

📌 Logical Reasoning as Part of Mathematics

• Logical reasoning is a branch of mathematics

• Traditionally, logic was expressed in natural language

Mathematical statements are often connected using phrases like:

• “because”
• “therefore”
• “if and only if”
• “a necessary condition is”

These phrases help in forming meaningful arguments

✔ Important concept:
Logic acts as the “glue” that connects different mathematical statements together

📌 Boolean Values in Logic

Logic is based on two fundamental values:

• True
• False

Every logical statement must result in one of these values.

PROPOSITIONS

📌 Definition

A proposition is:

A statement that is either true or false.

📌 Explanation

A proposition must:

• Clearly state something

• Have a definite truth value (True or False)

📌 Examples

• “It is raining” → can be true or false

• “I live in Lahore” → can be true or false

Therefore, both are propositions

📌 Non-Propositions

Some statements are not propositions because they do not have a truth value:

• Commands (e.g., “Do it”)

• Orders (e.g., “You must work hard”)

These cannot be true or false, so they are not propositions

📌 Atomic Propositions

Atomic propositions are:

Simple statements that cannot be divided into smaller parts

They form the basic building blocks of logic.

ROLE OF LOGIC IN PROPOSITIONS

Logic is not concerned with whether a statement is actually true in real life.

Instead, logic focuses on:

• Whether the reasoning is correct

• Whether the conclusion logically follows from given statements
📌 Example from Lecture

Statement:

“The knowledge in universities grows and grows. Each new student brings knowledge,
and graduates do not take any away.”

Breakdown:

Premises:

• Each new student brings knowledge

• Graduates do not take knowledge away

Conclusion:

• Knowledge increases

Explanation

Even if the structure seems logical, the argument may still be invalid in real life.

This shows:

• Logic checks structure of reasoning, not real-world truth

PROPOSITIONAL LOGIC

📌 Definition

Propositional logic is:

A system used to represent and analyze logical statements using propositions.

📌 Purpose

The main purpose of studying propositional logic is:

To model real-life situations in a way that allows formal reasoning

📌 Why We Study It

• To improve problem-solving ability

• To represent situations mathematically
• To check whether conclusions are valid or not

📌 Example 1 (From Lecture)

Statement:

“If the train arrives late and there are no taxis at the station, then John is late for his
meeting.”

Given:

• John is not late

• The train did arrive late

Conclusion:
There were taxis at the station

Explanation

This example shows how:

• Logical reasoning helps in deriving conclusions

• Even if information is incomplete, logic helps fill the gaps

📌 Example 2

Statement:

“If it is raining and Jane does not have her umbrella, then she will get wet.”

Given:

• Jane is not wet

• It is raining

Conclusion:
Jane has her umbrella
Explanation

This shows:

• Logical reasoning can be used to prove hidden facts

• It helps in analyzing real-life situations

MODELING

📌 Definition

Modeling is:

The process of converting real-world statements into logical or mathematical

formulas.

📌 Explanation

To analyze problems formally, we must:

1. Take English sentences

2. Convert them into variables (like p, q)
3. Represent relationships using logical structure

📌 Example

Statement:

“If it is raining and Jane does not have her umbrella, then she gets wet”

This can be represented as:

(raining AND no umbrella) → gets wet

📌 Importance of Modeling

• Makes reasoning precise and clear

• Allows use of mathematical techniques
• Helps verify whether an argument is valid or not
 FORMAL METHODS – LECTURE 03

PROPOSITIONS, EQUIVALENCE & PREDICATE LOGIC (THEORETICAL

NOTES)

PROPOSITIONS AND THEIR EQUIVALENCE

In software engineering, especially in SRS (Software Requirement Specification),

logical statements are used to clearly describe system requirements and behavior.

Propositions help in expressing conditions in a precise and unambiguous way, which is

very important in formal methods.

📌 Logical Equivalence in Propositions

Logical equivalence means that:

Two different logical expressions represent the same meaning and always produce
the same result.

📌 Implication and its Equivalence

A very important concept is:

An implication can be rewritten in another form without changing its meaning

Form:

p→q

Equivalent form:

¬p ∨ q

📌 Explanation

This means:

• If condition p happens, then q must happen

• OR if p does not happen, the condition still holds
 This equivalence is very useful in:

• Simplifying logical expressions

• Writing system requirements more clearly

📌 Concept of Contradiction in Systems

Sometimes a system may contain conditions that are logically impossible.

Example concept:
A condition where something is both enabled and disabled at the same time

This can be written as:

q ∧ ¬q

📌 Explanation

• Such a condition is always false

• It represents an invalid or conflicting requirement

In software systems, identifying such contradictions is very important to avoid errors.

📌 Simplification Using Equivalence

Logical equivalence helps in simplifying complex expressions by removing impossible

conditions.

Example idea:

• If a part of expression is always false, it does not affect the final result

This helps in making system logic:

• Cleaner
• Easier to understand
• Error-free

PROPOSITIONAL LOGIC
📌 Definition

Propositional logic is a system that deals with:

Simple statements and their combinations using logical relationships

📌 Explanation

It focuses on:

• Combining statements
• Evaluating their truth

It is useful for:

• Basic reasoning
• Simple system conditions

📌 Limitation of Propositional Logic

Propositional logic has limitations because:

• It cannot express detailed relationships between objects

• It cannot represent concepts like:
o “all”
o “some”
o “there exists”

📌 Conceptual Understanding

There are many real-world statements that require:

• Describing relationships between entities

• Expressing conditions about groups

Propositional logic is not powerful enough for this

PREDICATE LOGIC
📌 Definition

Predicate logic is:

A system that extends propositional logic by allowing statements about objects and
their relationships.

📌 Explanation

Predicate logic allows us to:

• Represent properties of objects

• Represent relationships between objects
• Use variables to generalize statements

📌 Role in Programming

In computer programs:

• Variables are used as placeholders

• These represent objects or values

Predicate logic helps in:

• Structuring complex conditions

• Modeling real-world problems

CONSTRUCTING PREDICATES FROM NATURAL LANGUAGE

To convert a natural language statement into predicate logic, a structured approach is

followed.

🔹 1. Identify Predicate

A predicate describes:

• A property of an object
OR
• A relationship between objects

It is the main logical component of the statement

🔹 2. Determine the Domain

Domain refers to:

The set of all objects being considered in the statement

🔹 3. Define Variables

Variables are:

• Symbols used to represent objects in the domain

They act as placeholders in logical expressions

🔹 4. Construct Predicate Formula

In this step:

• Predicates
• Variables
• Logical relationships

are combined to form a complete logical expression

QUANTIFIERS

📌 Definition

Quantifiers are used to specify:

How many elements in the domain satisfy a given condition

📌 Types of Quantifiers
🔹 Universal Quantifier (∀)

• Represents “for all”

• Indicates that a condition is true for every element
🔹 Existential Quantifier (∃)

• Represents “there exists”

• Indicates that a condition is true for at least one element

📌 Conceptual Understanding

Quantifiers help in expressing:

• General rules
• Partial truths

Without quantifiers, it is not possible to:

• Fully represent real-world conditions

TYPES OF PREDICATES

Predicates can be classified based on the number of arguments they take.

📌 Unary Predicate

• Takes only one argument

• Describes a property of a single object

📌 Binary Predicate

• Takes two arguments

• Describes a relationship between two objects

📌 Explanation

The number of arguments depends on:

• The complexity of the relationship being described

 ROLE OF PREDICATE LOGIC

Predicate logic is more powerful than propositional logic because:

• It can represent complex and detailed statements

• It can describe relationships between multiple objects
• It supports the use of quantifiers
• It allows better modeling of real-world systems

IMPORTANT CONCEPT ABOUT QUANTIFIERS

In logic, statements can describe:

• Conditions that are always true

• Conditions that are sometimes true

📌 Explanation

• If a condition is always true → universal case

• If it is true for some cases → existential case

This distinction is important in:

• Mathematical reasoning
• Software modeling

Z SCHEMA OVERVIEW (THEORETICAL NOTES ONLY)

1. INTRODUCTION TO Z SCHEMA

Z notation is a formal specification language used for designing and specifying

computer-based systems.

It is based on:

• Set Theory
• First-order Predicate Logic

Z notation provides:

• Mathematical precision
• Clear and unambiguous system description
 Z schemas are the core component used to structure formal specifications.

They help in defining:

• System data
• System behavior

2. BACKGROUND

Z notation was developed in the late 1970s at the University of Oxford.

Its purpose was:

• To support formal methods in software engineering

• To specify systems in a rigorous and structured manner

It allows:

• Early verification of system properties

• Detection of errors at early stages

Z schemas combine:

• Data structures
• Operations

This improves:

• Clarity
• Correctness

3. Z SCHEMA STRUCTURE

A Z schema is represented in a structured form and consists of two main parts:

📌 Declaration Part

• Introduces variables
• Defines their types

It represents the data of the system

📌 Predicate Part

• Specifies conditions or constraints on the variables

• Defines valid states of the system

📌 General Form

SchemaName
[declarations]
|
[predicates]

4. OPERATION SCHEMA

An operation schema describes:

The behavior of a system when an operation is performed

It defines:

• How the system state changes

• What inputs are required
• What conditions must be satisfied

📌 Important Concepts

• State changes are represented explicitly

• Input and output variables are defined
• Constraints ensure correct system behavior

📌 Key Notations

• Δ (Delta): Indicates that the system state is changing

• ? (Question mark): Represents input variables
• ' (Prime): Represents updated or new values after operation

FORMAL METHODS – PETRI NETS (DETAILED THEORETICAL NOTES)

 INTRODUCTION TO PETRI NET

Petri Net is a modeling technique used to study:

Dynamic and concurrent behavior of systems

📌 Explanation

• It is used for systems where:

o Multiple processes run at the same time (concurrent systems)
o Activities happen in steps (discrete flow)

It helps in understanding:

• System behavior
• Process interaction
• Flow of control

📌 Usage

Petri Nets are widely used in:

• Industry
• Academia
• Research

They are important for analyzing:

• Network-based systems
• Distributed systems

BASIC COMPONENTS OF PETRI NET

A Petri Net consists of two main types of nodes:

📌 1. Places

• Represent conditions or states

• A place can contain tokens
• A place may have:
o Zero tokens
 o One token
o Multiple tokens

📌 2. Transitions

• Represent events or actions

• Show changes in the system

📌 3. Arcs

• Connect:
o Place → Transition
o Transition → Place

Important:

• Direct connection between same types is NOT allowed

(Place → Place ❌, Transition → Transition ❌)

📌 4. Tokens

• Represent:
o Resources
o Data
o State markers

Tokens move in the system when transitions fire

📌 Graphical Representation

• Places → Circles
• Transitions → Bars/Rectangles
• Arcs → Arrows
• Tokens → Dots

BEHAVIOR OF PETRI NET

• A transition can fire (execute) when conditions are satisfied

• When a transition fires:
 o Tokens move from input places to output places

This represents change in system state

PROPERTIES OF PETRI NETS

🔹 1. Sequential Execution

One transition must occur before another

• Transition t2 can fire only after t1

• This creates order or precedence

✔ Meaning:

• Some actions must happen in sequence

🔹 2. Synchronization

A transition requires tokens from multiple places

• Transition fires only when:

o Each input place has at least one token

✔ Meaning:

• Multiple conditions must be satisfied together

🔹 3. Merging

Tokens from different places combine at one transition

✔ Meaning:

• Multiple inputs are processed by a single event

🔹 4. Concurrency

Multiple transitions can occur at the same time

✔ Meaning:

• System supports parallel execution

• Multiple processes run simultaneously

Important for:

• Distributed systems
• Multi-process systems

🔹 5. Conflict

Two or more transitions are ready to fire, but only one can occur

✔ Meaning:

• Choosing one transition disables the others

🔹 Conflict Resolution

Conflict can be resolved in two ways:

1. Non-deterministic
o Random selection
2. Probabilistic
o Selection based on assigned probabilities

Example idea:

• Either t1 or t2 occurs
• Or either t3 or t4 occurs