Formal Methods in Software Engineering
Lecture Slides 1
Asim Raza Fall 2012 Beaconhouse National University Lahore

Content
80% case studies
Pervades computer science, e.g., hardware circuit design, artificial intelligence, knowledge representation, database systems, programming languages, software engineering (design, verification, specification), … Will help you understand application of formal methods in computer science. i.e. Formal specifications in Z

Content
20% Theoretical study
Learn about history of formalism in mathematics and computer science Will help you understand advantages, limitations and other important issues of formal methods.

Logistics
Prerequisites:
Discrete Structures

Materials on course website, reachable from Moodle
Schedule of readings, home works, exams Lecture notes, available before class
Support for lectures

Logistics
Exams
Challenging, but not devious
All of the questions will be related to an example worked out in the text, a homework exercise, or a problem we did in class.

Logistics
Do readings before lecture (mandatory) Focus on various case studies that will be given for homework

Introduction to Formal Methods

What are Formal Methods
Area of computer science that is concerned with the application of mathematical techniques to the design and implementation of computer hardware and (more usually) software. OR
“That part of computer science concerned with the application of mathematical methods to the production of computer software”.

What are Formal Methods
Specification and verification methods Have formal (mathematical) semantics unambiguous facilitate proofs of correctness

In use since late 1970s more popular in Europe than US still only a niche market

Types of Formal Methods
Model-theoretic
VDM, Z

Algebraic
ACT One, Larch , OBJ

Concurrent processes
CCS, CSP, Petri Nets

Finite State Machines
Esterel, Statecharts

Hybrid
LOTOS, SDL

Types of Formal Methods
Property-based
Description of the operations that can be perform on a system, and the relationships between operations. More specifically: A signature part which de nes the syntax of operations (what parameters they take and return); An equations part, which de ne the semantics of the operations via a set of equations called axioms.

Model-based
Usage of the tools of set theory and first order predicate logic to build an abstract model of a system. You can then specify the operations that may be performed on your model, either explicitly, or implicitly (in terms of pre and postconditions). More specifically: A definition of the set of states a system may be in;

Types of Formal Methods
Property-based
Examples: Algebraic Specifications

Model-based dentitions for the legal operations that may be performed on your system, indicating how these change current state. The model we construct is: high-level; idealized; free of implementation bias (hopefully!) Examples: Z speci cation language VDM

Useful Key Terms
Specification:
Give a description of the system to be developed, and its properties in a mathematically defined syntax and semantics Concise description of high-level behavior and properties of a system System properties: Behavioral properties (Functional, timing, internal structures) Non-behavioral properties (security issues, constraints)

Useful Key Terms (cont’d)
States are described in rich math structures (set, relation, function)