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

of real-time systems. It provides a uniform way for the specification of both relative
and absolute timing of events . An elevator control system illustrates the development
process including static structure, dynamic behaviors and the weaving of time aspect
by integration of Informal Specification and formal Specification with aspect-oriented
approach.
We consider that every floor has a pair of direction lamps indicating that the eleva-
tor is moving up or down. There is only one floor button and one direction lamp in the
top floor and the bottom floor. Every floor has a sensor to monitor whether the eleva-
tor is arriving the floor.
We consider that the elevator is required to satisfy the following timing con-
straints[32]:
[T1] After the elevator has stopped at a particular floor, the elevator's door will
open no sooner than OPEN_MIN_TIME and no later than
OPEN_MAX_TIME.
[T2] After the elevator has stopped at a given floor the elevator's door will
normally stay open for a STAY_OPEN_NORMAL_TIME. However, if the
CloseDoorButton on board of the elevator is pressed before this timeout
expires, the door will close but no sooner than STAY_OPEN_MIN_TIME.
[T3] After the door is closed, the movement of the elevator can resume, but no
sooner than CLOSE_MIN_TIME, and no later than CLOSE_MAX_TIME.
Separation of Concerns from Elevator System
Several concerns can be separated from the elevator control system, such as time
aspect, control aspect, and concurrency aspect. The development process of the eleva-
tor control system is shown as Fig.3. However, in this paper we only simply consider
the time aspect, and will complete other aspects in our future work.
Fig. 3. The Development Process of The Elevator Control System
Structural Description Using Class Diagrams
The real-time feature of real-time systems can be modeled using UML by extending
stereotypes, tagged values, and constraints before. For example, timing constraints
can be added on the class to express the time feature in class diagram. But the imple-
mentation of the time feature were still scattered throughout, resulting in tangled code