Software Reliability Methods Chap1

This post series record my reading notes of Software Reliability Methods recommended by Yi Li.

Peled introduce the description of software reliability and its importance with some worries during the historical moment familiar to our generation, the step from 1999 to 2000.

Why we focous on the reliability (or correctness) of software?

• Computer systems control many aspects of modern lives.
• The software development has grown at an unprecedented pace.
• Large scale cooperation even in different locations leads to difficulty in controlling the quality.
• Rules of design can't prevent the existence of errors even with highly skilled programmers.

Let's go through the world of formal methods!

1.1 Formal Methods

Something about "formal".

Formal: As methods are based on mathematical theories.

Formal specification: Techniques to give precise and unambiguous description of systems.

Formal analysis: Techniques to verify that a system(implementation) satisfies its specification, or to systematially seek for failed cases.

Deductive software verification was a representative of methods in the early research which focus on the correctness of systems. Suggestions to the programs, starting from their formal specification and ending with actual code.(still considered as manual)

Notion of an invariant: a correctness assertion that needs to hold.

Some other words about software testing: most frequently used quality assurance, but it does not cover all the possible executions. Codes have been thoroughly tested can still contain errors. (MAYBE NO THOROUGH TEST)

Some Formal Methods Terminology

There exists different definition of term Verification, here lists the def in this book.

Verification: The process of applying a manual or an automatic technique that is supposed to establish whether the code either satisfies a given property or behaves in accordance with some higher-level description of it.

So activities of deductive verification and model checking are included, but not testing.

1.2 Developing and Acquiring Formal Methods

Understanding the limitations.

Scope, finite state systems of moderate size.

• guarantee correctness: usually with suspicion
• finding erros: usually preferred

The research in formal methods is relatively new.

Buid a verification tool needs considerable effort.

Issues and perspectives

(In the book)

• Project manager
• Head of quality assurance team
• Enginner(User)
• Formal methods researcher

1.3 Using Formal Methods

Using formal methods can achieve various goals:

• Obtain a common and formal description of a system.
• Find errors that are introduced during the development of systems.
• Be integrated with and assist in the development process.

Different stages of the development. | The earlier the better.

1.4 Applying Formal Methods

State space explosion: Effectiveness tends to diminish with the size of the checked object.

Compositional methods seem desirable by test separately and make conclusions, but difficult to achieve compositionality.

Clean-room development methodology.