In ASTRAL, a real-time system is described as a collection of state machine specifications, where each specification represents a process type of which there may be multiple statically generated instances. Each process instance in the system executes concurrently and asynchronously with all the other process instances. Additionally, a global specification contains declarations for types and constants that are shared among more than one process type, as well as assumptions about the global environment and critical requirements for the whole system. The figure below presents the syntactic structure for an ASTRAL specification.
An ASTRAL process specification consists of a sequence of levels. Each level is an abstract data type view of the system being specified. The first ("top level") view is a very abstract model of what constitutes the process (types, constants, variables), what the process does (state transitions), and the critical requirements the process must meet (invariants and schedules). Lower levels are increasingly more detailed with the lowest level corresponding closely to high level code.
The process being specified is thought of as being in various states, with one state differentiated from another by the values of its state variables, which can be changed only by means of state transitions. Transitions are described in terms of entry and exit assertions by using an extension of first-order predicate calculus. Transition entry assertions describe the constraints that state variables must satisfy in order for the transition to fire, while exit assertions describe the constraints that are fulfilled by state variables after the transition has fired. An explicit non-null duration is associated with each transition. Transitions are executed as soon as they are enabled (i.e. when their entry assertions are satisfied) assuming no other transition for that process instance is executing.
Every process can export both state variables and transitions; as a consequence, the former are readable by other processes while the latter are executable from the external environment. Processes communicate by broadcasting the values of exported variables and the start and end times of exported transitions.
In addition to specifying system state (through process variables and constants) and system evolution (through transitions), an ASTRAL specification also defines system critical requirements and assumptions on the behavior of the environment that interacts with the system. The behavior of the environment is expressed by means of environment clauses, which describe assumptions about the pattern of invocation of external transitions. Critical requirements are expressed by means of invariants and schedules. Invariants represent requirements that must hold in every state reachable from the initial state, no matter what the behavior of the external environment is, while schedules represent additional properties that must be satisfied provided that the external environment behaves as assumed.
The computational model for ASTRAL is based on nondeterministic state machines and assumes maximal parallelism, noninterruptable and nonoverlapping transitions in a single process instance, and implicit one-to-many (multi-cast) message passing communication. In what follows, the main features of ASTRAL are briefly introduced using the specification of the elevator control system.
The elevator system consists of three process type specifications: Elevator, Elevator_Button_Panel, and Floor_Button_Panel. The processes declaration,
PROCESSES the_elevator: Elevator, the_elevator_buttons: Elevator_Button_Panel, the_floor_buttons: array [1..n_floors] of Floor_Button_Panel,
which occurs in the global specification, declares that there is one instance of the Elevator process and one of the Elevator_Button_Panel process. In addition, there are n_floors static instances of the Floor_Button_Panel process type. Each of these is accessed as "the_floor_buttons[i]", where i is in the range 1 to n_floors.
ASTRAL is a strongly typed language. Integer, Real, Boolean, ID, and Time are the only primitive types. All other simple and constructed types used in a process specification must either be declared in the type section of that specification or must be declared in the global specification and explicitly imported by the process specification.
The type ID is one of the primitive types of ASTRAL. Every instance of a process type has a unique id. An instance can refer to its own id by using Self. There is also an ASTRAL specification function idtype(i), which returns the type of the process that is associated with the id i.
The global specification has three type declarations. The first two,
pos_integer: TYPEDEF i: integer (i > 0), pos_real: TYPEDEF r: real (r > 0),
declare pos_integer and pos_real to be subtypes of the integers and reals, respectively, that contain integers or reals greater than zero. The declaration
floor: TYPEDEF i: pos_integer (i <= n_floors)
similarly defines floor to be a positive integer in the range 1 to n_floors.
In ASTRAL, one state is differentiated from another by the values of the state variables, and it is the state variables that are referenced and/or modified by the state transitions. All of the state variables must be declared in the variable section of a process type specification.
A special variable called now is used to denote the current time. The value of now is zero at system initialization. ASTRAL specifications can refer to the current time (now) or to an absolute value for time that must be less than or equal to the current time. The ASTRAL specification function past is used to specify the value that an expression had at some time in the past. That is, past(E, t) represents the value that the expression E had at time t.
In the Elevator specification, there are five state variables. The first,
position: floor,
indicates the floor that the elevator currently resides on. The next four,
going_up, door_open, moving, door_moving: boolean,
indicate the direction of movement, the status of the elevator door, and whether or not the elevator and door are moving.
In ASTRAL, definitions are used to make the specification more readable. They may contain zero or more parameters. The request_above definition in the Elevator process,
DEFINE
request_above(f0: floor): boolean ==
EXISTS f: floor
( f > f0
& ( the_elevator_buttons.floor_requested(f)
| the_floor_buttons[f].up_requested
| the_floor_buttons[f].down_requested)),
is used as a shorthand for determining if a request is outstanding on any
button above the given floor.
The interface section of an ASTRAL process specification indicates which types, constants, and definitions declared in the global specification are used by the process, which variables and transitions exported by other processes are referenced, and which variables and transitions are exported by the process. These are specified by the import and export clauses.
State variables and transitions may be explicitly exported by a process, which makes the variable values and information about the transitions visible to other processes. Exported variables and transitions must be explicitly imported to be referenced in another process specification. Exported transitions are visible to the external environment and are executed in response to calls issued by the environment. The export clause for the Elevator_Button_Panel process,
EXPORT floor_requested, request_floor,
indicates that the value of floor_requested can be imported by other processes (in particular, by Elevator) and that the transition request_floor is made available to the external environment.
The import clause indicates which globally declared types, constants, and definitions are used by a process and which variables and transitions exported by other processes are referenced by this process. The import clause for the Elevator_Button_Panel process,
IMPORT floor, request_dur, clear_dur, the_elevator, the_elevator.position, the_elevator.door_open, the_elevator.door_moving,
indicates that the floor type declared in the elevator system's global specification is imported, as well as the global constants request_dur and clear_dur, and position, door_open, and door_moving, which are imported from the the_elevator instance of the Elevator process type.
The initial clause of a process specification expresses the restrictions on the initial state of the process type. That is, for each state variable it is necessary to express the restrictions that are to be placed on its initial value. The initial clause for the Elevator process,
INITIAL position = 1 & going_up & ~door_open & ~moving & ~door_moving,
indicates that the elevator is initially stopped on the first floor, with its door closed and up as its direction of movement.
ASTRAL transitions are used to specify the ways in which an instance of a process type can change from one state to another. A transition is composed of a header, an entry assertion, and an exit assertion. The header gives type information for the transition's parameters and specifies the amount of time required for the transition to execute. The entry assertion expresses the enabling conditions that must hold for the transition to occur, and the exit assertion specifies the resultant state after the transition occurs. That is, it specifies the values of the state variables in the new state relative to the values they had in the previous state.
In an ASTRAL specification, exceptions are dealt with explicitly. That is, a transition can have except/exit pairs in addition to the standard entry/exit pair. An except assertion expresses an exception that may occur when a transition is invoked. The corresponding exit assertion specifies the resultant state after the transition occurs. Each exception has its own duration, thus a transition may have a different execution time depending on whether it was invoked based on the entry assertion or on one of the exceptions.
A transition is executed as soon as its entry assertion is satisfied (assuming no other transition in that process instance is executing). If two or more transitions are enabled simultaneously, a nondeterministic choice will occur and only one of them will be executed. Whenever a process instance starts executing an exported transition, it broadcasts the start time and the values of the actual parameters to all interested processes (i.e. any process that has imported the transition). When the transition is completed, the end time as well as the new values of any exported variables that were modified by the transition are broadcast. Of course, any exported variables that are modified by a non-exported transition are also broadcast by the process when the transition completes execution. Thus, if a process is referencing the value of an imported variable while a transition is executing on the process instance exporting the variable, the value obtained is the value the variable had when the transition commenced. That is, the ASTRAL computation model views the values of all variables being modified by a transition as being changed by the transition in a single atomic action that occurs when the transition completes execution.
Start(T, t) is a predicate that is true if and only if transition T starts at time t and there is no other time after t and before the current time (now) when T starts (i.e. t is the time of the last firing of T). For simplicity, the functional notation Start(T) is adopted as a shorthand for "time t such that Start(T, t)" whenever the quantification of the variable t (whether existential or universal) is clear from the context. Startk(T) is used to give the start time of the kth previous occurrence of T. References to the end time of a transition T may be specified similarly using End(T) and Endk(T). The figure below illustrates the definition of Start for a transition T. In the interval [t1, t4), Start(T) = t1. At t4, however, Start(T) = t4 and Start2(T) = t1.
The close_door transition represents the time at which the elevator begins to close the door. The value close_dur is the execution time for this transition. The entry assertion expresses the fact that the elevator can only close the door when the door is open and stationary and the time since it became open is at least t_stop time into the past. Notice that in exit assertions, variable names followed by a prime (') indicate the value that the variable had when the transition began firing. The exit assertion expresses that the door of the elevator begins moving to the closed position.
TRANSITION close_door ENTRY [TIME: close_dur] door_open & ~door_moving & now - t_stop >= Change(door_open) EXIT door_moving
The close_door transition shows the use of the ASTRAL predicate Change, which is used to denote the last time that an expression has changed its value. That is, Change(E, t) is true if and only if the expression E has changed value at time t and there is no other time between t and the current time (now) at which the expression value has changed. Change follows syntactic conventions similar to Start and End, where Change(E) is the last time that the value of E changed and Changek(E) is the kth previous time that it changed.
Because ASTRAL is intended to be used for designing reactive systems, it is necessary to be able to express assumptions about the external environment in which the system operates. This is accomplished by using environment clauses, which formalize the assumptions that must hold on the behavior of the environment to guarantee certain desired system properties. These assumptions are expressed as first-order formulas involving calls to exported transitions. If T is an exported transition, Call(T) may be used in the environment clause to denote the time of the last occurrence of a call to T (with the same syntactic conventions as Start(T) and End(T)). Callk(T) denotes the time of the kth previous occurrence of a call. It should be noted that there may be a delay from the time a transition T is called until it is actually started. Also, if there are multiple calls to transition T before it fires, then Call(T) is the time of the first of these calls. The figure below illustrates the definition of Call for a transition T. In the interval shown, Call(T, t3) holds at and after t3. Calls to T that occur in the interval (t3, t4] are ignored since there is already a call to T outstanding.
There are both local and global environment clauses. Local environment clauses refer to a single instance of the process type they are associated with, while the global clause refers to the system as a whole. The environment of the Elevator_Button_Panel process type,
ENVIRONMENT Change(the_elevator.door_moving, now) & the_elevator.door_moving & the_elevator.door_open & the_floor_buttons[the_elevator.position] = Self -> FORALL t: time ( Change2(the_elevator.door_moving) ( t & t ( now -> ( past(the_elevator.going_up, t) -> ~Call(request_up, t)) & ( ~past(the_elevator.going_up, t) -> ~Call(request_down, t))),
states that requests cannot be made for the elevator to stop at a floor in the current direction of movement between when the door starts opening on that floor until when it starts closing. This assumption is necessary to prevent the elevator from being delayed indefinitely by repeatedly pressing the button at the elevator's current position before the door has closed, which would result in the door repeatedly opening and closing on the same floor without servicing other requests in the building.
ASTRAL also allows assumptions about the system context provided by other processes in the system to be expressed in the imported variable clause. This clause describes patterns of changes to the values of imported variables, including timing information about any transitions exported by other processes that may be used by the process being specified (e.g. Start(T) and End(T)). The imported variable clause is optional and is not an essential part of an ASTRAL specification. It is used to aid in proving the correctness of a system in a modular fashion. The figure below illustrates the difference between imported variable assumptions and environment assumptions. Imported variable assumptions are made about entities within the system, while environment assumptions are made about those that are outside.
The portion of the imported variable clause of the Elevator process type,
IMPORTED VARIABLE FORALL f: floor ( Change(the_elevator_buttons.floor_requested(f), now) & ~the_elevator_buttons.floor_requested(f) -> EXISTS t: time ( Change2(the_elevator_buttons.floor_requested(f)) < t & t <= now & past(position, t) = f & ~past(door_open, t) & past(door_moving, t))),
states that a button on the elevator button panel only clears after the elevator has arrived and started opening the doors. This assumption is necessary so that the buttons do not get cleared just before the elevator arrives at a floor and then get requested again after it leaves, causing the elevator to skip the floor, thus delaying the service time.
For a real-time system, there are two types of critical requirements: behavioral and temporal. In ASTRAL, both types are expressed in the invariants, constraints, and schedules.
The invariants express the critical requirements that are to hold in every reachable state. That is, they express properties that must initially be true and must be guaranteed to hold during system evolution. The invariant for the Elevator process,
INVARIANT moving -> ~door_open & ~door_moving,
states that whenever the elevator is moving, the elevator door must stay closed.
The constraints express the critical requirements that must hold between any two states that correspond to the start and end of a transition. The requirements contained in a constraint could be expressed in an invariant. Thus, the constraint is just a notational convenience. Invariants can be global or local, where global invariants represent properties that need to hold for the system as a whole, while local invariants and constraints defined at the process type level represent properties that must hold for each process instance. Invariant and constraint properties must be true regardless of the environment or context in which the process or system is running. The constraint for the Elevator process,
CONSTRAINT (going_up & ~going_up' -> ~request_below'(position')) & (~going_up & going_up' -> ~request_above'(position')),
states that whenever the elevator changes direction, there cannot have been a request outstanding in the old direction when the decision was made.
Schedules are additional system properties that are required to hold under more restrictive hypotheses than invariants and constraints. Like invariants, schedules may be either local or global and obey similar scope rules. Unlike invariants, however, they express requirements that are to hold provided the environment and system context produce stimuli as prescribed in the environment and imported variable clauses.
Process schedule clauses deal with timing requirements for that process only. A process schedule cannot prescribe the values of variables for another process. It may refer only to calls to its own exported transitions and references to the values of imported variables from another process. The portion of the global schedule,
SCHEDULE FORALL f: floor ( the_elevator_buttons.Call(request_floor(f), now - t_service_request) -> EXISTS t: time ( now - t_service_request < t & t <= now & past(the_elevator.position, t) = f & Change(the_elevator.door_open, t) & past(the_elevator.door_open, t))),
states that whenever a request is made on the elevator button panel for the elevator to stop at a given floor, the elevator must arrive at that floor and open the door less than t_service_request time afterward.
Schedules are not required to be proved using the basic elements of an ASTRAL specification. It is important, however, to know that the schedule is feasible. There may be several ways to assure that a schedule is satisfied, such as giving one transition priority over another or making additional assumptions about the environment. Even though this kind of decision should often be postponed until a more detailed design phase, it is important to know that if further restrictions are placed on the specification and/or if further assumptions are made about the environment, then the schedule could be satisfied. For this reason, a further assumptions and restrictions clause can be included as part of a process specification. Unlike other components of an ASTRAL specification, this clause is only used as guidance to the implementer and is not a hard requirement.
The further assumptions and restrictions clause consists of two parts: a further environment assumptions section and a further process assumptions section. The further environment assumptions section obeys the same syntactic rules as the local environment. It states further hypotheses on the admissible behaviors of the environment interacting with the system. The further process assumptions section restricts the possible system implementations by specifying suitable selection policies in the case of nondeterministic choice between several enabled transitions, transition selection, or by further restricting constants, constant refinement. In general, the further process assumptions reduce the level of nondeterminism of the system specification.
An ASTRAL process specification consists of a sequence of levels where the behavior of each level is implemented by the next lower level in the sequence. Given two ASTRAL process level specifications PU a nd PL, where PL is a refinement of PU, the implementation statement IMPL defines a mapping from all the types, constants, variables, and transitions of PU into their corresponding terms in PL. A type, constant, variable, or transition of PL representing the implementation of a corresponding term in PU i s referred to as a mapped type, constant, variable, or transition. PL can also introduce types, constants and/or variables that are not mapped. These are referred to as the new types, constants, or variables of PL. Note that PL cannot introduce any new transitions (i.e. each transition of PL must be a mapped transition). A transition of PU can be mapped into a sequence of transitions, a selection of transitions, or any combinations thereof.
A selection mapping of the form TU == A1 & TL.1 | A2 & TL.2 | ... | An & TL.n, is defined such that when the upper level transition TU fires, one and only one lower level transition TL.j fires, where TL.j can only fire when both its entry assertion and its associated "guard" Aj are true. A sequence mapping of the form TU == WHEN EntryL DO TL.1 BEFORE TL.2 BEFORE ... BEFORE TL.n OD, defines a mapping such that the sequence of transition TL.1; ...; TL.n is enabled (i.e. can start) whenever EntryL evaluates to true. Once the sequence has started, it cannot be interrupted until all of its transitions have been executed in order. The starting time of the upper level transition TU corresponds to the starting time of the sequence (which is not necessarily equal to the starting time of TL.1 because of a possible delay between the time when the sequence starts and the time when TL.1 becomes enabled), while the ending time of TU corresponds to the ending time of the last transition in t he sequence, TL.n. Note that the only transition that can modify the value of a mapped variable is the last transition in the sequence. This further constraint is a consequence of the ASTRAL communication model. That is, in the upper level, the new values of the variables affected by TU are broadcast when TU terminates. Th us, mapped variables of PL can be modified only when the sequence implementing TU ends.
The interlevel proofs consist of showing that the mapping for each upper level transition is correctly implemented by the corresponding sequence, selection, or combination thereof in the next lower level. For selections, it must be shown that whenever the upper level transition TU fires, one of the lower level transitions TL.j fires, that the effect of each TL.j is equivalent to the effect of TU, and that the duration of each TL.j is equal to the duration of TU. For sequences, it must be shown that the sequence is enabled if and only if TU is enabled, that the effect of the sequence is equivalent to the effect of TU, and that the duration of the sequence (including any initial delay after EntryL is true) is equal to the duration of TU. The details of transition mappings and process refinement are presented in [CKM 95].
To facilitate reuse and to simplify the construction of large and complex real-time systems, ASTRAL provides the developer with a composition capability. The ASTRAL compose clause contains the necessary information to combine two or more ASTRAL system specifications (i.e. a global specification and its associated collection of process specifications) into a single specification of the combined system. If S1 and S2 denote two ASTRAL top level specifications, then the interaction between the processes of S1 and S2 is described by specifying which exported transitions of the processes of S1 and S2 are no longer exported to the external environment. That is, the stimuli needed to fire these transitions in S1 are produced by processes of the sibling system S2 and vice-versa, rather than by the external environment.
Figure (a) below shows two systems, S1 and S2. S1 exports transitions T1 and T2 and state variables x1, x2, and x3, while S2 exports transition T3 and state variables y1 and y2. When S1 and S2 are composed, some transitions of S1 will not require an external call, since S2 is now providing part of the environment in which S1 works. This works similarly for some transitions of S2. For instance, in figure (b) below, transitions T1 and T3 are no longer exported, since the events that trigger them are now represented by particular values of y2 and x1, x3, respectively. Thus, the composed system, C, will export only transition T2. That is, the external environment of C can call only transition T2 (see figure (c) below).
a) b) c)
The most important part of the compose section is the call generation clause, which describes how exported transitions of S1 processes are triggered by events occurring in S2 processes and vice-versa. These events are described by formulas of the following form:
FORALL t: Time,... (P(S1) <-> Call(T, t)),
where P(S1) is an ASTRAL well-formed formula describing the occurrence of the events in S1 that are equivalent to calling the exported transition T of S2. For example, suppose the composition section contains the following call generation clause (taken from [CGK 97]):
FORALL t: Time, C: Central_Control_ID, L: Line
( Change(LD_Unit(C).LocStatus(L), t)
& LD_Unit(C).LocStatus(L) = In_Progress
<-> C.Call(Receive_LD(LD_Unit(C).LocOut(L)),t))
This means that whenever the variable LD_Unit(C).LocStatus(L) changes to In_Progress, an "internal call" is made to Receive_LD. The details of the composition clause and the process of automatically composing ASTRAL specifications are presented in [CK 93].
| [CGK 97] | A. Coen-Porisini, C. Ghezzi, and R.A. Kemmerer. "Specification of realtime systems using ASTRAL". IEEE Transactions on Software Engineering, Sept. 1997, vol. 23, (no. 9): 572-98. |
| [CK 93] | A. Coen-Porisini and R.A. Kemmerer. "The composability of ASTRAL realtime specifications". International Symposium on Software Testing and Analysis, Cambridge, MA, USA, 28-30 June 1993. SIGSOFT Software Engineering Notes, July 1993, vol. 18, (no. 3): 128-38. |
| [CKM 95] | A. Coen-Porisini, R.A. Kemmerer, and D. Mandrioli. "A formal framework for ASTRAL inter-level proof obligations". Proceedings of the 5th European Software Engineering Conference, Sitges, Spain, 25-28 Sept. 1995. Berlin, Germany: Springer-Verlag, 1995. p. 90-108. |
Richard Kemmerer / kemm@cs.ucsb.edu
URL: http://www.cs.ucsb.edu/~astral/lang.html
last update: 7-27-99