Page 192 - DCAP507_SYSTEM_SOFTWARE

System Software

Notes 2. Verification: As affirmed above, formal methods vary from other specification systems
by their heavy stress on provability and accuracy. By building a system with a formal
specification, the designer is in fact developing a set of theorems about his system.
By proving these theorems accurate, the formal Verification is a tricky process, largely
since even the simplest system has several dozen theorems, each of which has to be
proven. Even a traditional mathematical proof is a multifaceted affair.

Example: Wiles' proof of Fermat's Last Theorem, for example, took some years after its
declaration to be completed. Given the demands of complexity and Moore's law, approximately
all formal systems use an automated theorem proving tool of some form. These tools can show
simple theorems, verify the semantics of theorems, and give assistance for verifying more
complex proofs.
3. Implementation: Once the model has been stated and verified, it is implemented by
transforming the specification into code. As the dissimilarity between software and
hardware design increases, narrower, formal methods for producing embedded systems
have been developed.

Example: LARCH, for example, has a VHDL implementation. Likewise hardware systems
like the VIPER and AAMP5 processors have been produced using formal approaches.
An substitute to this approach is the lightweight approach to formal design. In a lightweight
design, formal methods are applied cautiously to a system. This approach provides the benefits
of formal specification, but also averts some of the difficulties.
Formal methods are observed with a definite degree of suspicion. While formal methods research
has been succeeding since 1960's, formal methods are only being slowly acknowledged by
engineers. There are numerous reasons for this, but most of the problems appear to be a result
of misapplication. Most formal systems are tremendously descriptive and all-encompassing,
modeling languages have usually been judged by their capacity to model anything. Regrettably,
these same qualities make formal methods very tricky to use, especially for engineers untaught
in the type theory required for most formal systems.
In opposition, it is noticeable that some form of formal specification is essential: complex
systems need formal models. In addition, the mathematics needed for formal methods is
becoming a more prominent fixture of engineering curricula, engineering schools in Europe are
already requiring courses in VDM, Z and alike formal specifications. Eventually, formal methods
will acquire some form of acceptance, but compromises will be made in both directions: formal
methods will turn out to be simpler and formal methods training will turn out to be more
common.
Formal methods propose additional benefits outside of provability, and these advantages do
deserve some mention. However, most of these advantages are available from other systems,
and usually without the steep learning curve that formal methods require.
 Discipline: By virtue of their rigor, formal systems require an engineer to think out his
design in a more thorough fashion. In particular, a formal proof of correctness is going to
require a rigorous specification of goals, not just operation. This thorough approach can
help identify faulty reasoning far previous than in traditional design. The discipline
included in formal specification has proved functional even on already obtainable systems.

Example: Engineers by means of the PVS system, for example, reported identifying
numerous microcode errors in one of their microprocessor designs.

186 LOVELY PROFESSIONAL UNIVERSITY