Predictability in real-time software design
Jinfeng Huang · TU/e Research Portal · 2005
ion and refinement are two elementary transformations performed during the design process (as shown in Figure 2.2). Abstraction is the activity that tries to remove (or hide) irrelevant information, which improves the comprehensibility of existing design models and facilitates the evaluation of different design solutions. The major goal of abstraction activities is to improve the understandability of the Effective design transformations 19 Figure 2.2: Basic design activities design, thereby assisting designers to make correct design decisions. Refinement is the activity that adds more implementation details to models, thereby reducing the gap between models and realizations. The major goal of refinement activities is implementability. Intuitively speaking, abstraction activities intend to clarify what the system (component) can do, while refinement activities intend to clarify how the functionality of the system (component) can be achieved. We can see from Figure 2.2 that an intermediate design outcome (model) plays dual roles in the design process. It is the abstraction of its lower-level design outcomes and the refinement of its higher-level design outcomes. In other words, it states what the functionality of the lower-level outcomes is and describes how the functionality of the higher-level design outcomes can be implemented. It is natural to see that the top-level of the design process in Figure 2.2 refers to desired properties (requirements), while the bottom-level refers to a realization. Actually, the design process indeed intends to fill the gap between the desired properties (what the system should be) and the realization (how the system functions). Now the question arises on what condition two design outcomes form an abstraction/refinement pair. In design practice, we can use the following principle. System A is an abstraction of B (thus B is the refinement of A) iff for any desired property p, if p is satisfied by A, then p is also satisfied by B. In a specific formal framework, a more formal definition can be given. For example, in a state trace based formal framework, each property or model can be interpreted as a set of state traces. The satisfaction relation between a model and a property is defined by the inclusion relation between their corresponding sets of state traces. A refinement actually restricts the set of state traces of a model into one of its subsets. If the set of state traces of the property includes that of the abstraction, then it should also include the set of state traces of the refinement. This is consistent with our abstraction/refinement principle. Note that Figure 2.2 only gives a single flow of refinement and abstraction transformations. In practice, the design process can be much more complex than depicted in Figure 2.2. Figure 2.3 presents an example of a transformational design process, where the design objective is to devise a realization satisfying five properties P0 till 20 Design approaches for real-time software P0 P1 P2 P4 P3 Properties