Aspect-Oriented Formal Specification for Real-Time Systems - Advances in Computational Science and Engineering - page 16

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