Page 252 - DCAP305_PRINCIPLES_OF_SOFTWARE_ENGINEERING

Principles of Software Engineering

Notes Figure 12.3: The Verification Refactoring Process

Proof Checker transformation
to library

Specify & prove
new transformation Select Transformation
transformation Library

Original Apply
Specification User Guidance transformation

Implementation Proof
Verified Specification Extraction Metric Metric Transformed Transformer Code
Yes Implecation Proof Yes met? Analyzer Code
No No Statically collect & Mechanically check &
Later verification proofs
analyze code properties apply transformation

We are not aware of any transformations or circumstances of their application in which a
transformation would have to be removed, and we make no explicit provision for removal in the
current tools and process. In the event that it becomes necessary, removing a transformation is
achieved easily by recording the software’s state prior to the application of each transform. All
the user activities, especially the design and selection of transformations, have to be mechanically
checked, and these two activities need to support by automation to the extent possible. The
transformer is implemented using the Stratego/XT toolset. Stratego checks the applicability of
the selected transformation, and carries it out mechanically using term rewriting. We use the
PVS theorem proven as the transformation proof checker and provide a proof template. When
the user specifies a new transformation, an equivalence theorem will be generated automatically,
and the user can discharge it interactively in the theorem proverb.

The term “bug” was used in an account by computer pioneer Grace Hopper (in
1946), who publicized the cause of a malfunction in an early electromechanical
computer.

12.3 Software Metrics

Software cannot be seen nor touched, but it is essential to the successful use of computers. It is
necessary that the reliability of software should be measured and evaluated, as it is in hardware.
IEEE 610.12-1990 defines reliability as “The ability of a system or component to perform its
required functions under stated conditions for a specified period of time.” IEEE 982.1-1988defines
Software Reliability Management as “The process of optimizing the reliability of software through
a program that emphasizes software error prevention, fault detection and removal, and the use
of measurements to maximize reliability in light of project constraints such as resources, schedule
and performance.” Using these definitions, software reliability is comprised of three activities:
1. Error prevention

2. Fault detection and removal
3. Measurements to maximize reliability, specifically measures that support the first two
Activities there have been extensive work in measuring reliability using mean time between
failure and mean time to failure.

Successful modelling has been done to predict error rates and Software metrics have been proved
to reflects the software quality, and thus has been widely used in software quality evaluation
methods. The results of these evaluation methods can be used to indicate which parts of a

246 LOVELY PROFESSIONAL UNIVERSITY