Scribd
Upload
115 views

Formal Transforamtion - Processs Model

The document discusses the formal transformation approach to software engineering. Formal transformation is a mathematically-based technique for specifying, developing, and verifying software and hardware systems similar to the waterfall model. It involves expressing requirements and design mathematically and using formal logic for implementation and testing. Advantages include being precise and error-free, suitable for safety-critical systems, and having correctness proofs. Disadvantages include being time-consuming, expensive, and requiring specialized expertise. Formal transformation has applications in areas like routers, operating systems, and security and is used for specification, development, verification, and proving properties of systems.

Uploaded by

kid unique
Copyright
© © All Rights Reserved
We take content rights seriously. If you suspect this is your content, claim it here.
Available Formats
Download as PPTX, PDF, TXT or read online on Scribd
115 views

Formal Transforamtion - Processs Model

The document discusses the formal transformation approach to software engineering. Formal transformation is a mathematically-based technique for specifying, developing, and verifying software and hardware systems similar to the waterfall model. It involves expressing requirements and design mathematically and using formal logic for implementation and testing. Advantages include being precise and error-free, suitable for safety-critical systems, and having correctness proofs. Disadvantages include being time-consuming, expensive, and requiring specialized expertise. Formal transformation has applications in areas like routers, operating systems, and security and is used for specification, development, verification, and proving properties of systems.

Uploaded by

kid unique
Copyright
© © All Rights Reserved
We take content rights seriously. If you suspect this is your content, claim it here.
Available Formats
Download as PPTX, PDF, TXT or read online on Scribd
You are on page 1/ 15

A

A Formal
Formal Transformation
Transformation
Approach
Approach to
to Software
Software
Engineer
Engineer

Group Members:
Nathaniel Dakin
Tavoy Savery
Steven Mcfarlane
Software Development Life Cycle

• A software development life cycle (SDLC) model is a


conceptual framework describing all activities in a
software development project from planning to
maintenance. This process is associated with several
models, each including a variety of tasks and activities.
• Software life cycle models describe phases of the
software cycle and the order in which those phases are
executed. There are many different types of models,
and many companies adopt their own, but all have very
similar patterns.
Formal Transformation Diagram
Formal Specification: The
Requirements
Requirements software requirements and
Definition specifications are combined in
Definition this phased and expressed
mathematically
Formal
Specification Formal Transformation :
The design
implementation and unit
Formal testing are done in this
phase using
Transformation mathematical notation

Integration and
System Testing Maintenance
What is Formal Transformation ?

• Formal Transformation is a particular kind of


mathematically based technique for the specification,
development and verification oh hardware and
software systems.

• It is similar to the waterfall model (where one phase


flows into the next and must be completed before the
next phase is started) but it’s specification is converted
to a mathematical module and based on functions
which are defined using mathematical notations.
Examples of the Formal
Transformation method ?
• B- Method- based around AMN (Abstract Machine
Notation), which is used in the development of
computer software. It supports development of
programming language code from specifications.

• VDM (Vienna Development Method)- one of the


first established formal methods.

• RAISE (Rigorous Approach to Industrial Software


Engineering)- consist of a set of tools based around
a specification language (RSL) for software
development.
Examples of the Formal
Transformation method ?
• ATP (Automated Theorem Proving or
Automated Deduction)- is the proving of
mathematical theorems by a computer program.

• Petri Nets (Place/Transition Nets ) – Petri Nets


have an exact mathematically definition of their
execution semantics with well developed
mathematical theory for process analysis.
Advantages of The Formal
Transformation method
• It is precise and free of errors
Formal Transformations are said to be error free due to
the numerous mathematical specifications which do not
allow room for error

• It is said to be suitable for safety critical system


Due to its error free nature, this ensures that the system
runs as intended without any bugs or glitches that will
affect the running of any vulnerable systems.

• It has correctness proof


Formal Transformation has proven that a program will
operate properly .
Disadvantages of The Formal
Transformation method

• Very costly

• It is very complexed.

• Requires specialized expertise due to its


complexed nature
Summary of Disadvantages and Advantages of The
Formal Transformation Method

Advantages Disadvantages
• Time consuming and
• Discovers ambiguity , expensive
incompleteness, and • Difficult to use this model as
inconsistency in the software. a communication mechanism
• Offers defect free software for non technical personnel
• Incrementally grows in effective • Extensive training is required
solutions after each iteration since only few developers
• This model does not involve high have the essential knowledge
complexity rate to implement this model
• Formal specification language
semantic verify self- consistency
Applications of The Formal
Transformation method
Formal methods are applied in different areas of hardware and
software, including:
• Routers
• Ethernet Switches
• Routing Protocols
• Security Applications
• Operating Systems Microkernels

Formal verification has been frequently used in hardware by most


of the well-known hardware vendors, such as IBM, Intel, and
AMD. There are many areas of hardware, where Intel have used
FMs to verify the working of the products, such as parameterized
verification of cache coherent protocol, Intel Core i7 processor
execution engine validation and optimization for Intel IA-64
architecture using HOL light theorem prover
Uses of The Formal
Transformation method
Formal methods can be applied at various points through the development process.

• Specification - Formal methods may be used to give a description of the system


to be developed, at whatever level(s) of detail desired. This formal description
can be used to guide further development activities additionally, it can be used
to verify that the requirements for the system being developed have been
completely and accurately specified or formalizing system requirements by
expressing them in a formal language with a precise and unambiguously
defined syntax and semantics.

• Development - Formal development using formal methods as an integrated part


of a tool-supported system development process. If the formal specification is in
an operational semantics, the observed behavior of the concrete system can be
compared with the behavior of the specification. Additionally, the operational
commands of the specification may be amenable to direct translation into
executable code.
Uses of The Formal Transformation
method (Cont’d)
• Verification - Formal verification using a software tool to prove properties of a
formal specification, or that a formal model of a system implementation satisfies
its specification.

 Sign-off verification - A formal verification tool for sign-off verification is a tool


that is highly trusted such that it can replace traditional verification methods (the
tool may even be certified).

 Human-directed proof - Sometimes, the motivation for proving the correctness of


a system is not the obvious need for reassurance of the correctness of the system,
but a desire to understand the system better. Consequently, some proofs of
correctness are produced in the style of mathematical proof: handwritten (or
typeset) using natural language, using a level of informality common to such
proofs. A "good" proof is one which is readable and understandable by other
human readers.

 Automated proof - In contrast, there is increasing interest in producing proofs of


correctness of such systems by automated means , in which a system attempts to
produce a formal proof from scratch, given a description of the system, a set of
logical axioms, and a set of inference rules.

You might also like