Categories

A sample text widget

Etiam pulvinar consectetur dolor sed malesuada. Ut convallis euismod dolor nec pretium. Nunc ut tristique massa.

Nam sodales mi vitae dolor ullamcorper et vulputate enim accumsan. Morbi orci magna, tincidunt vitae molestie nec, molestie at mi. Nulla nulla lorem, suscipit in posuere in, interdum non magna.

Overview of Formal Methods – Foundation for analysis methods

Formal methods provide a foundation for specification environments leading to analysis models that are more complete, consistent, and unambiguous than those produced using conventional or object-oriented methods. The descriptive facilities of set theory and logic notation enable a software engineer to create a clear statement of facts.

The underlying concepts that govern formal methods are :
– the data invariant, a condition true throughout the execution of the system that contains a collection of data.
– the state, a representation of a system’s externally observable mode of behavior, or the stored data that a system accesses and alters.
– the operation, an action that takes place in a system and reads or writes data to a state. An operation is associated with two conditions : a precondition and a postcondition.

Discrete mathematics – the notation and heuristics associated with sets and constructive specification, set operators, logic operators, and sequences – forms the basis of formal methods. Discrete mathematics is implemented in the context of formal specification languages, such as OCL and Z. These formal specification languages have both syntactic and semantic domains. The syntactic domain uses a symbology that is closely aligned with the notation of sets and predicate calculus. The semantic domain enables the language to express requirements in a concise manner.

A decision to use formal methods should consider startup costs as well as the cultural changes associated with a radically different technology. In most instances, formal methods have highest payoff for safety-critical and business-critical systems.

Where are Formal Methods applied?
Although a complete formal verification of a large complex system is impractical at this time, formal methods are applied to various aspects, or properties, of large systems. More commonly, they are applied to the detailed specification, design, and verification of critical parts of large systems such as avionics and aerospace systems, and to small, safety-critical systems such as heart monitors.

Leave a Reply

You can use these HTML tags

<a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <s> <strike> <strong>