Information Technology Reference

In-Depth Information

they provide a means to symbolically examine the entire state space of a digital design

(whether hardware or software) and establish a correctness or safety property that is true

for all possible inputs. Although the use of mathematical logic is a unifying theme

across the discipline of formal methods, there is no single best "formal method". Each

application domain requires different modeling methods and different proof approaches.

Furthermore, even within a particular application domain, different phases of the life

cycle may be best served by different tools and techniques. For example a theorem

prover might be best used to analyze the correctness of a RTL [21] level description of a

Fast Fourier Transform circuit, whereas algebraic derivational methods [8][22] might

best be used to analyze the correctness of the design refinements into a gate-level de-

sign. Therefore there are a large number of formal methods under development

throughout the world. Formal methods in software draw upon some advanced mathe-

matics. Mathematical topics of interest include formal logic, set theory, formal lan-

guages, and automata. Formal methods support precise and rigorous specifications of

those aspects of a computer system capable of being expressed in the available formal

languages. Since defining what a system should do, and understanding the implications

of these decisions, is the most troublesome problems in software engineering, this use of

formal methods has major benefits.

Many of the existing models used to specify functional system behavior - opera-

tional techniques such as automata [23], Petri nets [12], process algebra [[26], and

descriptive techniques like logics [25] - have been enriched by means to express

non-functional real-time properties. Some work of is based on variants of timed

automata.[23] Time restrictions are introduced by labeling transitions or states of

extended finite state machines with time limits, clocks and time variables. An upper

bound
u
and a lower bound
l
is assigned to each transition of the timed automaton.

Once enabled, the transition may be executed not sooner than
l
and not later than
u

time units after the enabling. Similar conditions for the enabling of transitions can

be formulated referring to the values of time variables. These are model-theoretic

techniques in that they distinguish all execution sequences of a system into those

that satisfy the timing constraints the ''good'' ones, and those that do not satisfy

them the ''bad'' ones. Only those systems that can only reveal ''good'' execution

sequences implement the specification. Similar timed extensions have been defined

for Petri Nets, Time
Petri Nets, Object Composition Petri Nets and Time Stream

Petri Nets. There have also been numerous real-time extensions to process algebras,

a process algebra-based QoS specification language based on the FDT LOTOS has

been proposed. Temporal logics are the descriptive counterpart to specifying state

transition systems by automata. Temporal logics specify qualitative temporal rela-

tionships between states. A program satisfies temporal logic specifications if all of

its execution state sequences satisfy these temporal relations. As can be expected,

extensions have been introduced to augment temporal logics with constructs that

specify quantitative real-time relations between states. Examples are Metric Tempo-

ral Logic MTL and Quality of Service Temporal Logic QTL [11] that use real-time

interval annotations to the temporal operators, and techniques introducing explicit

timer variables as in Real-Time Temporal Logic RTTL or Temporal Logic of Ac-

tions TLA. LOTOS is used to specify the functional requirements and multimedia

Search WWH ::

Custom Search