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

Supporting specification and analysis of a system from multiple aspects to capture
different perspectives on a system,
Providing methods and tools that are appropriate for different aspects for improved
understandability of specifications,
Employing a formal basis to integrate multiple aspects and perform analyses with
mathematical rigor,
And providing methods to handle the size and complexity required by large-scale
systems.
When specifying real-time systems, decomposition and composition are the pri-
mary methods for coping with complexity. Typically, decomposition can be done in
two orthogonal dimensions. First, the system is decomposed in the vertical dimension
by partitioning the real-time system into loosely coupled subsystems with well-
defined interfaces. Each subsystem is then decomposed further in the horizontal di-
mension usually in a top-down fashion. However, with this approach it is easy to
introduce unnecessary complexity due to two facts. Firstly, the interfaces between
subsystems are defined before capturing their collective behavior. Secondly, applica-
tion-specific parts, that crosscut the two dimensions, are scattered around in different
components of the subsystems. Furthermore, they are tangled with other parts. In
recent years the recognition of problems related with scattering and tangling in object-
oriented software systems has led to an introduction of an aspect-oriented design
methodology enabling different, possibly overlapping, design concerns to be decom-
posed separately before composing them together. Aspect-oriented approaches use a
separation of concern strategy, in which a set of simpler models, each built for a spe-
cific aspect of the system, are defined and analyzed. Each aspect model can be con-
structed and evolved relatively independently from other aspect models. This has
three implications:
Firstly, an aspect model can focus on only one type of property, without burden of
complexity from other aspects. Hence an aspect model is potentially much simpler
and smaller than a traditional mixed system model. This is expected to dramatically
reduce the complexity of understanding, change, and analysis.
Secondly, different levels of detail or abstraction can be used in the construction of
different aspect models. This allows us to leverage of existing understanding of cer-
tain aspect of the system to reduce the complexity of modeling and analysis. For ex-
ample, if the timing property of a component/subsystem is well understood, we can
build an extremely simple timing model for the component.
Lastly, existing formal notations normally are suitable for describing one or a few
types of system properties. By adopting the aspect concept, we can select the most
suitable notation to describe a given aspect. Likewise, we can select the most suitable
analysis techniques to analyze a given property.
Formal Methods refers to mathematically rigorous techniques and tools for the speci-
fication, design and verification of software and hardware systems. The phrase "mathe-
matically rigorous" means that the specifications used in formal methods are
well-formed statements in a mathematical logic and that the formal verifications are
rigorous deductions in that logic (i.e. each step follows from a rule of inference and
hence can be checked by a mechanical process.) The value of formal methods is that