Page 193 - DCAP507_SYSTEM_SOFTWARE

Unit 12: Formal Systems and Programming Languages

 Precision: Conventionally, disciplines have moved into jargons and formal notation as Notes
the weak spots of natural language descriptions turn out to be more clearly obvious.
There is no motive that systems engineering should vary, and there are numerous formal
methods which are used almost exclusively for notation.
For engineers designing safety-critical systems, the advantages of formal methods lie in their
clearness. Unlike many other design strategies, the formal verification needs very clearly defined
goals and strategies.

Did u know? In a safety critical system, vagueness can be extremely dangerous, and one of
the main benefits of the formal approach is the removal of ambiguity.

Task Make distinction between verification and implementation.
Self Assessment

Fill in the blanks:
1. A formal system comprises a formal language and a set of .............................. rules.
2. .............................. are system design methods that use thoroughly declared mathematical
models to construct software and hardware systems.
3. Formal methods vary from other design systems via the use of formal ..............................
systems.

4. Modeling languages are .............................. grammars which permit users to model complex
structures out of predefined types.
5. Once the model has been stated and verified, it is implemented by transforming the
.............................. into code.

12.2 Formal Specifications

 A formal specification is a requirement articulated in a language whose vocabulary, syntax
and semantics are formally defined.

!
Caution It cannot be depend on natural language but as an alternative must be based on
mathematics.

12.2.1 Advantages of Formal Specifications

 The development of a formal specification offers insights into and understanding of the
software needs and the software design.
 Given a formal system requirement and a complete formal programming language
definition, it may be probable to establish that a program conforms to its specification.

 Formal specifications have the possibility of automated processing.

LOVELY PROFESSIONAL UNIVERSITY 187