COMP7730: Formal Methods in Software Engineering
Levent Yilmaz
[email protected]
1
Outline
 Overview of the syllabus
 http://www.eng.auburn.edu/~yilmaz/comp7730
 Introduction to formal methods
 Why formal methods
 A historical perspective
 Myths about formal methods
2
Introduction to formal methods
Jeannette M. Wing (1990). A specifier’s introduction to formal
methods. IEEE Computer, 23(9):8-24, September 1990.
 Formal methods are mathematically based techniques that provide
frameworks within which people can
 specify,
 develop, and
 verify systems in a systematic, rather than ad-hoc manner.
 They provide the means of
 proving that a system has been implemented correctly,
 proving properties of a system without necessarily running it.
3
High quality software
 The importance of high quality software
 What are the characteristics of high
quality software?
 The need for precision in the specification
of software
4
Top 10 excuses for low
quality software
Top 10 Replies by Programmers when their programs do not work:
10. "That's weird..."
9. "It's never done that before."
8. "It worked yesterday."
7. "It must be a hardware problem."
6. “I haven't touched that module in weeks!"
5. "You must have the wrong version."
4. "Somebody must have changed my code."
3. "Did you check for a virus on your system?"
2. "You can't use that version on your system."
And the Number One Reply by Programmers when their programs don't work:
1. "I thought I fixed that."
5
The need to produce correct software
systems
 As computers become cheaper, smaller, and
more powerful, their spread through our
technological society becomes more
pervasive.
6
Why study formal
methods?
The software industry has a long standing and well earned reputation for failing to deliver on its promises. In
the September 1994 issue of Scientific American, a number of sobering examples are given and it is
observed that "despite 50 years of progress, the software industry remains years -- perhaps decades -short of the mature engineering discipline needed to meet the needs of an information-age society."
In an article in the January/February 1997 issue of I.E.E.E. Software, Luqi and Goguen cite staggering cost
estimates of software development failures at $81 billion for 1995, and $100 billion for 1996.
In his Web article, Goguen calls attention to several highly visible failures: the cancellation of IBM's $8 billion
contract with the FAA for a new nation-wide air control system, the DOD cancellation of a $2 billion
contract with IBM to modernize its information systems, the failure of the software for delivering real-time
sports data at the 1996 Olympics, the one and one-half year delay in the United Airlines automated
baggage handling system at the new Denver airport at a cost of $1.1 million per day, and the list could
go on.
A reading of Peter Neumann's book, Computer Related Risks, will reveal that such problems are not at all
new, although they appear to be growing. Neumann even points out deaths which resulted from radiation
overdoses from a computer-based radiation-therapy system in the mid-1980s
It is clear that there is no price that can assure the success of software projects with the current technology.
For large complex projects an ad hoc approach has proven inadequate. The lack of formalization in key
places makes software engineering overly sensitive to the foibles that are inevitable in the highly
technical and detailed activities associated with software creation. Aids to precision and cross-checking
are essential, and this is precisely the objective of formal methods.
7
The role of formal methods
 Formal methods reveal ambiguities,
incompleteness, and inconsistencies.
 One tangible product of applying a formal method is
a formal specification.
 Specification languages - <Syn, Sem, Sat>


Syntactic domains, Semantic domains, and
Satisfies relation
 Desirable properties of specifications
 Proving properties of specificands
8
Pragmatics
 Users
 Uses




Requirements analysis
System design
System verification and validation
System documentation
9
Characteristics




Model vs. property oriented
Visual languages
Executable
Tool-support
10
A historical perspective
 Syntax – necessary but insufficient to
describe the meaning of programs.
 Testing – What is wrong with program
testing?
 Verification – The modern concept of
program verification was first introduced by
Floyd in 1967.
11
The Floyd verification model
12
A brief survey of techniques
 Axiomatic specification and verification
 Weakest preconditions
 Guarded commands
 Algebraic specification
 Statecharts and model checking
13
Limitations of formal methods
Myth 1: formal methods guarantee perfect software and
eliminate the need for testing.
Myth 2: formal methods are all about proving programs correct.
Myth 3: formal methods are only useful in safety-critical
systems.
Myth 4: application of formal methods requires highly trained
mathematicians.
Myth 5: applications of formal methods increases development
costs.
Myth 6: formal methods are unacceptable to users.
Myth 7: formal methods are not used on real large-scale
systems.
14
Model-based SpecificationWhat is Z?
 Z is a formal specification language for
software systems. It supports
 Representational and
 Procedural abstraction
 In Z operations are specified by their
input/output behavior.
15
Descargar

Slide 1