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!
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)
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.
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.
(In the book)
- Project manager
- Head of quality assurance team
- Formal methods researcher
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.
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.
本博客所有文章除特别声明外，均采用 CC BY-SA 4.0 协议 ，转载请注明出处！