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)…