Abstract

We develop a formal specification of an animation data model for exploration of dynamic Geographic Information Systems. Specifically, we treat the description of temporal composition of complex behavior and the coordination of multiple changes of states. The conceptualization of the model represents animations through an increasing abstraction of the animated objects’ behavior. Animations are built up constructively from the lowest to the highest level of abstraction in the model, based on operations that permit the composition and manipulation of complex behaviors. Entities with high-level abstractions and reasonable set of operations allow users to easily combine and manipulate animations, creating a new view of the environment, which is more suitable for the exploration and investigation of unusual behavior.

CR Categories and Subject Descriptors: I.3.7 [Computer Graphics]: Three-Dimensional Graphics and Realism – Animation; I.6.8 [Simulation and Modeling]: Types of Simulation – Animations.

Keywords: Geographic information systems, animation, data model, formal specification, and virtual reality.

1 INTRODUCTION

Like many scientific graphic-intensive applications, geographic information systems (GISs) are migrating from a two-dimensional desktop environment to an immersive, three-dimensional, dynamic, virtual-reality environment (MacEachren et al. 1999; Dam et al. 2000). GIS developers and users can now walk or fly through a three-dimensional representation of the information, interact with the environment, and explore the dynamic behavior of geographic phenomena via animations (Raper 2000). By interaction we mean the change of a characteristic of an object in response to the user’s action or position. By animation we mean the time-varying representation of one or more attributes of an object in which an observer can sense the variation using any sensory channel.

Animation and interaction are important mechanisms for the visualization and analysis of dynamic phenomena; therefore, they are helpful in the cognitive process of the virtual exploration of an environment. Simply animating, however, the information available in a spatio-temporal database, while allowing the user to explore the animation by mimicking VCR operations (e.g., play, stop, forward, backward), does not offer the full understanding of the world. Users are constrained to seeing animations in which the number of animated objects in a scene can easily exceed the users' capacity to understand the dynamic environment. Although some applications do allow users to perform a selective view of an animation by choosing a few groups of objects to participate in the animation (Manoharan et al. 2002), this selection is solely based on the judgment of the user and does not consider temporal or causal relations among the objects. In this way, some important behaviors can be inadvertently hidden so that they are not taken into account in the cognitive process of the virtual exploration of animations.

In a virtual exploration of a multi-dimensional environment with space and time, the limited mechanism to control and manipulate animations is no longer acceptable. Users should have the opportunity to explore temporal and causal relations between objects. Our work focuses on the model of the virtual exploration of animations. Our goal is to provide a formal specification of an animation data model so that users can combine and manipulate animations to gain insight and discover relationships. With such tools the users will be able to create their own views of the dynamic environment.

The remainder of this paper is structured as follows: Section 2 discusses the framework used by current animation models and proposes the extension of this framework to incorporate operations to support the manipulation of animations and causal relations. Section 3 presents some features of the formal specification. Section 4 presents a formal specification of an animation model. Section 5 draws conclusions and discusses future works.

2 ANIMATION FRAMEWORK

The scientific visualization community has proposed many different data models (Zeleznik et al. 1991; Strauss and Carey 1992; Najork and Brown 1995; Green and Halliday 1996; Elliott and Hudak 1997; Luttermann and Grauer 1999) to represent time variation of information through animations. An analysis of many data models that support computer animations shows an emphasis on rapid developments of prototypes and portability between applications, but shows little support for manipulations of an animation, with a naive notion of causality. The majority of proposed specifications partitions animation into three main logical parts (Lee 1998), which clearly identify the animated objects (who), the actions these objects undergo (what), and the times during which the objects undergo the actions (when). The conceptualization of an animation data model based on the Who-What-When framework has led to implementations with very low levels of abstraction and without sufficient information and methods to combine and manipulate animations. The focus of such models is the presentation of the animation, but the animation is difficult to maintain as the number of objects or the complexity of the behavior increases. Likewise, such an animation is difficult to manipulate without a reasonable representation of the animation.

We extend the Who-What-When framework to support the representation of causal relations between objects and actions (why) and to incorporate methods to combine and manipulate animations that deal with different representations of objects (how). The why-part of the framework captures causal relations between objects and their behaviors and provides methods to manipulate animations based on such relations. The how-part of the framework provides methods to (1) combine and manipulate complex behaviors, (2) explore temporal relations among simple behaviors to compose complex animations, (3) coordinate multiple state changes, and (4) manage the animation of different representations of the same object. The emphasis of this paper is on a conceptualization and specification of an animation model with methods to compose and manipulate animations based on temporal relations and the coordination of multiple changes. In the future, this work will be further extended with operations to support causality, interaction, and different representations of the same object.

The goal of our animation model is to provide a high-level abstraction of the object behavior and to identify a reasonable set of operations that allow users to easily combine and manipulate such behaviors, creating a new view of the dynamic environment. The intended audience of this model is engineers and GIS analysts. These kinds of users are less interested in realistic representations and unpredictable behaviors of objects, such as those used in cinematographic animations and interactive computer games (Funge et al. 1999). The animation model requires that the entire behavior of an object is known ahead of time. In this way the model can act as a post-processor of a simulation application or as a front-end of a spatio-temporal database. In the exploration of a dynamic virtual environment, the fact that the result of the animation needs to be known a priori cannot be considered a disadvantage. Users need to have complete control over animations to take full advantage of this rich representation. It is possible only if the behavior of the objects is known in advance. Animations that run in parallel with simulation applications cannot be manipulated, as they are constrained by the pace of the simulation and compete with the simulator for CPU usage (Henriksen 1999).

3 FORMAL SPECIFICATION

It has been argued that formal specification—a powerful mechanism to represent software design intentions—are the only way to rigorously define correctness of a computer program (Astesiano and Kreowski 1999). Specifications state what needs to be done without premature choices stating how it should be done. A good specification is accomplished through a wise description of a theory located somewhere between ambiguity and over-constraint. The specification should be restrictive enough to avoid implementations that are unacceptable, while it should be unrestrictive enough to allow for efficient and elegant implementations. Although the use of formal specification proved valuable in the design of graphical applications (Mallgren 1982), animation models have typically been presented only through informal means.

Algebraic specification is one kind of formal specification techniques. There are many languages used to express a specification using algebraic specifications. The selection of an appropriate language depends on the context of use and the range of applications. One of the most successful specification language is Larch (Guttag et al. 1993). Larch is an algebraic specification language with a theory based on many-sorted first-order logic with equality. In this paper we present our specification with Java Modeling Language (JML) (Leavens et al. 2000a). JML is a behavioral interface specification language for the Java programming language (Arnold and Gosling 1998). JML adapted the model-based approach of Larch by using specification-only model fields. These fields describe abstractly the value of objects and are used only for the purposes of the specification. The predicates in JML are written using regular Java expressions extended with logical operators and universal and existential quantifiers (Huisman 2001). This approach gives JML the expressiveness of Larch interface language's family and has the advantage to free specifiers and readers of dealing with the Larch's dry algebraic-style.

JML uses an annotation style, which permits the specification to be embedded in regular Java files. JML specifications are surrounded by annotations markers (i.e., /*@ and @*/). Thus, JML annotations are treated as comments by Java compilers, but are relevant for JML type checkers (Leavens et al. 1999), program static checker (Leavens et al. 2000b), and theorem proffers (Jacobs et al. 1998).

Figure 1 shows a JML specification (Leavens et al. 2000a) of a method of the class IntMathOps that contains a static method that returns the integer part of the squared root of the argument. The text below does not shows how to compute the desired result but it must appear in every program that correctly implements this specification. It is behind the scope of this paper to present the JML syntax. For more details about the JML language see: http://www.cs.iastate.edu/~leavens/JML.html.

public class IntMathOps {

/*@ public normal_behavior

@ requires y >= 0;

@ ensures \result * \result <= y && y < (Math.abs(\result) + 1) *

@ (Math.abs(\result) + 1);

@*/

public static int isqrt(int y);

}

Figure 1. An example of a JML specification.

4 ANIMATION MODEL

The complex theory associated with the animation data model cannot be presented in a few pages using just a single specification. In order to enhance the understanding of this model, its specification needs to be divided into smaller modules. We use only a subset of the whole specification to discuss some relevant concepts of the model. In this way, the theory associated with each specification module is consistent, but it is not complete in the sense of formal specifications. In this paper, we will rely on the reader’s knowledge of the application domain to deal with the incompleteness of the specification.

The modules of the animation model (Figure 2) represent increasing abstractions of the animated objects’ behaviors. Animations are built up constructively from the lowest to the highest level of abstraction in the model. The high levels of abstraction (i.e., the modules Course of Action and Animation) allow users to easily manipulate the behavior of an object and to combine and manipulate animations, creating a new view of the environment that is more suitable for the exploration and investigation of unusual behavior.

Figure 2. Modules of the animation model specification.

State Type represents types of attributes for which the user can sense the variation. Normalized Act, Timed Act, and Course of Actions represent different stages of the behavior of the animated phenomena. Animation aggregates pairs of Course of Actions and VR objects representing the dynamic environment. VR object is an abstraction that represents the graphical presentation of the animated object. The unique restriction applied to these objects is that they need to be compatible with the Course of Actions (i.e., the object needs to have all attributes being animated in the Course of Actions).

4.1 State Type Specification

The basic module of the model is a State Type. State Type is an abstraction that represents the types of attributes to be animated. The State Type specification (Figure 3) has a model field _types, which is declared as a mathematical set of elements of the sort AttributeType. AttributeType represents any kind of attribute of objects in which users can sense variations (e.g., position, scale, rotation, color, texture, or shape). State Types can have one or more types of attribute. The Empty State Type (i.e., State Type without type) is not allowed in the model. These characteristics are defined by the invariant clause in the specification. The method isRelated defines the notion of related State Types. Two State Types are related if they have at least one AttributeType in common. The definition of related types represents an important concept in this model and will be fully understood in the context of coordination of multiple changes of states, discussed later in this paper.

public /*@ pure @*/ class StateType {

/* @ public model JMLValueSet _types;

@ public invariant _types != null !_types.isEmpty();

@ && (\forall JMLType t; _types.has(t); t instanceof AttributeType);

@*/

/* @ public normal_behavior

@ requires (attType instanceof AttributeType) && (attType!=null);

@ assignable _types;

@ ensures _types.equals(\old(_types.insert(attType)));

@ ensures_redundantly \old(_types.has(attType)) ==> _types == \old(_types);

@*/

public void insert (AttributeType attType);

/*@ public normal_behavior

@ requires statetype instanceof StateType && StateType != null;

@ ensures \result <==>

@ (\exists AttributeType at1; _types.has(at1);

@ (\exists AttributeType at2;statetype.getTypes().has(at2);

@ at1.equals(at2)));

@*/

public /*@ pure model@*/ boolean isRelated (StateType statetype);

/* @ public normal_behavior

@ requires _types != null;

@ ensures \result == _types;

@*/

public /*@ pure @*/ JMLValueSet getTypes();

}

Figure 3. Formal specification of State Type.

4.2 Specifications of Normalized and Timed Acts

A Normalized Act is an abstraction that is defined over a normalized time space, composed of a State Type (_stateType), an ordered sequence of State Values(_stateValues), and Normalized Times (_stateTime), and an interpolation function that generates intermediate state values of the act. These information are represented by model fields in specifications (Figure 4). The State Value and Normalized Time specifications are straightforward. State Value is an abstraction that represents values for every type defined by the State Type of the act. Times associated with State Values are of the sort Normalized Time (i.e., they are elements of the normalized temporal space). The collection of representative state values and the times during which they hold are stored in the model and can be seen as the keyframes of the animation.

Following the declaration of the model fields there is a constraint clause. This clause is used to say how values can change between publicly-visible states (Wing 1987), that is, the constraint clause states that the number of keyframes is the same in the pre and post-state. The invariant clauses in the specification define some additional features of normalized acts. For instance, the minimum number of keyframes in an act is 2. The first and last keyframe hold at the normalized times 0 and 1, respectively. Others keyframes, if they exist, hold in the interval between 0 and 1, exclusively. These constraints guarantee that the act is defined over the entire normalized temporal space. The last invariant clause states that there do not exist two state values that hold at the same time.

public class NormalizedAct {

/*@

@ public model StateType _stateType;

@ public model StateValue[] _stateValues;

@ public model NormalizedTime[] _stateTimes;

@ public model int _numberKeyframes;

@ public constraint _numberKeyframes == \old(_numberKeyframes);

@ public invariant _numberKeyframes >= 2;

@ public invariant (\forall int index;index >=0 && index <=_numberKeyframes-1;

@ _stateTimes[index] instanceof NormalizedTime);

@ public invariant _stateTimes[0] == (new NormalizedTime(0))

@ && _stateTimes[_numberKeyframes-1] == (new NormalizedTime(1));

@ public invariant (\forall int ind1;ind1 >=0 && ind1 <=_numberKeyframes-1;

@ (\forall int ind2;ind2>index1 && ind2<=_numberKeyframes;

@ _stateTimes[index1].getTime!=_stateTimes[index2].getTime));

@*/

/*@ public normal_behavior

@ requires st!=null && sv0!=null && sv1!=null;

@ assignable _stateType,_stateValues,_stateTimes,_numberKeyframes;

@ ensures _stateType == st && _stateValues[0] == sv0 && _stateValues[1] == sv1

@ && _stateTimes[0] == new NormalizedTime(0)

@ && _stateTimes[1] == new NormalizedTime(1)

@ && _numberKeyframes == 2;

@*/

public NormalizedAct (StateType st, StateValue sv0, StateValue sv1);

/*@ public normal_behavior

@ requires st != null && sv != null && nt != null;

@ requires_redundantly nk >= 2;

@ assignable _stateType,_stateValues,_stateTimes,_numberKeyframes;

@ ensures _stateType == st && _stateValues == sv

@ && _stateTimes == nt && _numberKeyframes == nk;

@ ensures_redundantly _stateTimes[0] == new NormalizedTime(0)

@ && _stateTimes[_numberKeyframes-1] == new NormalizedTime(1);

@*/

public NormalizedAct(StateType st, int nk, StateValue[] sv, NormalizedTime[] nt);

/*@ public normal_behavior

@ {|

@ requires hasStateTime(nt);

@ ensures hasStateValue(\result);

@ also

@ requires !hasStateTime(nt);

@ ensures !hasStateValue(\result);

@ |}

@ for_example

@ requires nt.getTime() == 0;

@ ensures \result == _stateValues[0];

@ also

@ requires nt.getTime() == 1;

@ ensures \result == _stateValues[_numberKeyframes-1];

@*/

public StateValue interpolator(NormalizedTime nt, String Order);

}

Figure 4. Formal specification of Normalized Act.

Following the invariant clauses there is the specification of two constructors of the type Normalized Act. The first constructor is used to create a Normalized Act with two keyframes only. The second constructor creates a Normalized Act with multiple keyframes. It is worth to note the use of ensures_rendundantly clauses in both constructors. This clause signaled checktable redundancy in the specification. It says that the description of the property is believed to follow from other properties of the specification, in our case, from the invariant clauses.

The last method of the Normalized Act specification describes the interpolator operation, which define the functionality of the interpolation function. The interpolation function is used to generate intermediate state values of Normalized Acts (i.e., state values between keyframes). The interpolation function can generate intermediate values in the normal and reverse sequence defined in the act. Other assertions and inherit specifications guarantee that the interpolation function is defined only over the normalized temporal space and that if normalized times associated with keyframes are used as parameters, the interpolation function returns the state value stored in the model. The specification of the interpolator method uses for_example clause that is an another way to add checktable redundancy to a specification. Assertions defining the reverseInterpolator operation are not presented. In this way there is no way to guarantee that the reverse sequence is generated coherently. The specification also abstracts away the details of how to compute the intermediate frames of the act, because it is an implementation issue.

A Timed Act extends the Normalized Act theory by adding operations to define the duration of the Timed Act (Figure 5). Such operations are equivalent to a temporal scale over the normalized space and define the pace of the evolution of Timed Acts.

The method defining the operation isConcurrent describes when two acts are concurrent. According to the axiom, two acts are concurrent when their associated State Types are related (i.e., concurrent acts have at least one type of attribute in common). The method isConcurrent is also critical in the context of coordination of multiple changes of states, which we treat in the specification of the module Course of Actions. The fact that two acts are concurrent does not imply that they are competing to interpolate the same attribute. This situation only occurs if the acts compete and occur at the same time.

public class TimedAct {

/*@ public model NormalizedAct _normalAct;

@ public model long _duration;

@ public invariant _duration>=0;

@*/

/*@ public normal_behavior

@ requires tAct!=null;

@ ensures \result ==_normalAct.getStateType().isRelated(

@ tAct.getNormalizedAct().getStateType());

@*/

public boolean isConcurrent (TimedAct tAct);

}

Figure 5. Formal specification of Timed Acts.

Normalized and Timed Acts are abstractions that represent a transition of states over time. There is no object associated with an act. For instance, the act that captures the movement of a ball can be used to represent the same movement of every object moving in the same pattern, enhancing the reusability of such a representation.

The reason to keep separate specifications for Normalized and Timed Acts is that they have a well-defined role in the model. While Normalized Act defines the pattern of the behavior and generates intermediate frames of the animations, Timed Act manages the pace of the animation and gives information for the coordination of multiple changes of states performed by in Course of Action abstraction. Such a distinction enforces the understanding of the model and facilitates the manipulation of these entities at a high level of abstraction.

4.3 Model of Time

Normalized Act, Timed Act, Course of Actions, and Animation have their own temporal model. All of them have a simple linear model of time, that is, they define simple intervals in their respective time spaces (Figure 6).

Normalized Acts define an interval over a normalized temporal space (t_na), whereas Timed Acts define an interval resulting from the mapping of Normalized Acts over the positive space. Normalized Acts are mapped onto the Timed Act space (t_ac) by specifying their duration. Such a mapping is equivalent to performing a scaling of the normalized space. In this way, both intervals have their starting time coinciding with the origin of their respective coordinate system.

Figure 6. Temporal models of Normalized Acts, Timed Acts, Course of Actions, and Animations.

Course of Actions defines a simple interval resulting from the combination of Timed Acts. Timed Acts are positioned along the Course of Actions timeline (t_ca) by specifying their absolute start point on the Course of Actions space or by specifying a temporal relation between existing Timed Acts. Such a transformation is equivalent to performing a translation of the Timed Act space. When the temporal relation changes the duration of the Timed Act a scale transformation is also performed over such an interval. Courses of Actions are combined together with VR objects to form more abstract entities, called Animations. Animation also defines an interval in the animation space, where the origin of the animation space coincides with the start time of the application. Courses of Actions are mapped onto the animation space (t_an) in a similar fashion, by specifying a start point in the Animation domain or through temporal relations between existing Courses of Actions. Thus, a direct mapping of the Course of Actions space onto the Animation space starts the animation as soon as the animation time reaches the start point of the first Course of Actions in the set. For all practical purposes, when the start point of the Course of Actions does not coincide with the origin of their coordinate system, there is a delay in the start of the animation.

Normalized and Timed Acts are coherent with the intuitive notion of intervals, a time associated with some event occurring in the world (Allen and Ferguson 1997). Course of Actions and Animation, on the other hand, do not fit well with this notion. We can have a Course of Actions or an Animation composed by Timed Acts or Courses of Actions, respectively, which do not meet or overlap, implying a period of inactivity inside the interval. The advantage of reducing such entities to a simple interval is that we can use the same set of operations that operate over intervals uniformly throughout the entire model. Operations used to combine Timed Acts to form a Course of Actions have the same functionality as (1) operations used to combine Courses of Actions to form an Animation; and (2) operations used to combine Animations to form an even more complex Animation.

4.3.1 Temporal Relations between Intervals

The process of combining intervals by simply specifying their absolute start time in the target time space is time consuming, susceptible to errors, and hard to maintain. For instance, if someone wants to change the start point of a specific Timed Act in a Course of Action and keep the temporal configuration of existing Timed Acts, the user also needs to change the start point of all intervals. Exploring temporal relations between time periods (Little and Ghafoor 1993; Weiss et al. 1995; Varzirgiannis and Sellis ) is a more natural way to position intervals and has the desired side effect of keeping the start points of existing intervals updated automatically. Users can manipulate Courses of Actions and Animations by imposing a temporal relation between intervals rather than specifying an absolute start time for each interval.

Given two temporal intervals (a and b), there exist thirteen possible relations that may hold between those intervals (Allen 1983) (Figure 7). Although all temporal relations have a significant role in the animation model, only some of them can be used to position a new interval unambiguously. An operation used to position an interval by imposing a temporal relation needs to constrain at least one of the end point of the new interval. Temporal relations meets, starts, finishes, and their converse relations, constrain one endpoint of the new interval. The temporal relation equals constrains the start and end points of the new interval (i.e., equals also constrains the duration of the new interval). Thus, operations that impose these temporal relations between intervals can be used to compose complex behaviors in an easy and natural way.

Figure 7: Temporal relations between intervals.

Other three-dimensional animation models have explored the use of temporal relations between intervals (Fiume et al. 1987; Dollner and Hinrichs 1997). These models, however, are primarily concerned with the development and presentation of the animation. The set of operations proposed in such models acts over low-level abstractions of objects’ behavior. Thus, they are not suitable to be manipulated by users on the fly. The major problem of these models, however, is that operations used to combine intervals do not constrain concurrent activities between their arguments, a critical issue in keyframe animations.

4.4 Course of Actions Specification

If the phenomenon has a complex behavior, includes a period of inactivity, or needs different interpolation functions between segments, a simple act can no longer be used. In order to model complex behaviors we need to combine acts. A Course of Actions is a combination of Timed Acts.

Consider the movement of a ball (Figure 8a). The ball rolls over the table, falls on the floor, bounces two times, continues to travel in a straight line, and then stops. One can imagine an interpolation function able to generate the entire movement of the ball. Such a function, although mathematically sound, cannot be readily accomplished. Another approach is to divide the entire movement of the ball into acts, which have a known interpolation function. Those acts are combined forming the Course of Actions of the ball.

Figure 8. (a) complex movement of a ball and (b) graphical representation of the Course of Actions of the movement of a ball.

The entire movement of the ball can be easily represented using five simple Timed Acts (Figure 8b). The Course of Action is modeled by adding each Timed Act and specifying its start time in the Course of Actions domain. The start point of the second Timed Act coincides with the endpoint of the first one, and so forth. This constraint guarantees the continuous and coherent flow of the movement. There is no requirement that one act follows another in a Course of Actions, although in our example, it is a desirable effect.

The specification of the module Course of Actions describes operations used to create and maintain Courses of Actions. The Course of Action specification starts with definitions of some model fields (Figure 9). Model fields _start, _end, and _duration represent the boundaries of the Course of Actions interval and are updated every time a new timed act is inserted. Timed Acts together with an instant in the Course of Action temporal domain are elements of the TimedActPositioned abstraction. These objects are stored in the Course of Action in a mathematical set called _timedActs. The clauses depends and represents are used to make assertions relating fields of the specification. The clause depends indicates that _end is dependent of _start and _duration (i.e., whenever _start or _duration change, _end always changes). The represents clause says how the value of _end is related with the values of _start and _duration.

The first invariant of the specification states that elements of the set _timedActs are of the sort TimedActPositioned. The second invariant of the specification states that does not exist two Timed Acts in the Course of Action which compete among themselves. The last invariant clause requires that the duration of the course of action to be greater than zero for every publicly-visibly state.

public class CourseOfAction {

/*@ public model JMLValueSet _timedActs;

@ public model long _start;

@ public model long _end;

@ public model long _duration;

@ public depends _end <- _start,_duration;

@ public represents _end <- _start+_duration;

@ public invariant _timedActs != null

@ && (\forall JMLType t; _timedActs.has(t); t instanceof

@ TimedActPositioned);

@ public invariant (\forall TimedActPositioned tap1; _timedActs.has(tap1);

@ (\forall TimedActPositioned tap2;

@ _timedActs.has(tap2) && !tap1.equals(tap2);

@ !compete(tap1,tap2)));

@ public invariant _duration >= 0;

@*/

Figure 9. Formal specification of Course of Actions.

Courses of Actions are abstractions that represent the entire behavior of an object. So, if the object has a complex behavior, it is reasonable to think about Course of Actions with periods of inactivity or with periods of simultaneous activities. The first situation holds when exists a temporal separation between Timed Acts defining the Course of Actions. The second situation holds when the intersection of the intervals of two or more Timed Acts is not the empty set, implying simultaneous activities inside the Course of Actions. The management of simultaneous activities is accomplished in an elegant way. The Course of Actions avoids the coexistence of two Timed Acts that compete. Two Timed Acts compete when they are concurrent and have a temporal relation of overlaps, overlappedBy, starts, startsBy, contains, containedBy, finishes, finishedBy, or equals holding between them. The pure method compete verifies when two TimedActs compete. Figure 10 depicts the specification of compete and two methods (i.e., before and after) used to verify the temporal relation between TimedActs. Since these methods are pure they can be used in assertion of the specification.

/*@ public normal_behavior

@ requires tActPos1!=null && tActPos2!=null;

@ ensures \result <==>

@ tActPos1.getTimedAct().isConcurrent(tActPos2.getTimedAct())

@ && (overlaps(tActPos1,tActPos2) || overlappedBy(tActPos1,tActPos2)

@ || starts(tActPos1,tActPos2) || startsBy(tActPos1,tActPos2)

@ || contains(tActPos1,tActPos2) || containedBy(tActPos1,tActPos2)

@ || finishes(tActPos1,tActPos2) || finishedBy(tActPos1,tActPos2)

@ || equals(tActPos1,tActPos2));

@*/

public boolean /*@pure model@*/ compete(TimedActPositioned tActPos1,

TimedActPositioned tActPos2);

/*@ public normal_behavior

@ requires _timedActs.has(tActPos1) && _timedActs.has(tActPos2);

@ ensures \result <==>

@ tActPos1.getPosition()+tActPos1.getTimedAct().getDuration()

@ < tActPos2.getPosition();

@*/

public /*@pure model@*/ boolean before( TimedActPositioned tActPos1,

TimedActPositioned tActPos2);

/*@ public normal_behavior

@ requires _timedActs.has(tActPos1) && _timedActs.has(tActPos2);

@ ensures \result <==> before(tActPos2,tActPos1);

@*/

public /*@pure model@*/ boolean after(TimedActPositioned tActPos1,

TimedActPositioned tActPos2);

Figure 10. Formal specification of the methods compete, before, and after.

In order to allow for the relative positioning of Timed Acts, the Course of Actions specification needs to be extended with methods, which support the relative inclusion of Timed Acts by specifying a temporal relation with an existing Time Act in the Course of Action (Figure 11). These methods position a new Timed Act by constraining at least one of the end points of the new interval by imposing a temporal relation between the new Timed Act and a Timed Act used as reference interval. The names of methods were modified by the prefix make to emphasize that we are imposing the temporal relation, rather than verifying whether the relation holds for the given periods. For the sake of simplicity we omitted assertions about the post-state of the start and duration of the Course of Action interval and the side effects generates by these methods in entities with a low level of abstraction in the model.

/*@ public normal_behavior

@ requires _timedActs.has(refAct) && _timedActs.has(repAct);

@ assignable _start,_duration;

@ ensures repAct.getPosition() =

@ refAct.getPosition()+refAct.getTimedAct().getDuration()

@ && _start == \old(_start);

@ ensures_redundantly meets(refAct,repAct);

@*/

public /*@model@*/ void makeMeets(TimedActPositioned refAct,

TimedActPositioned repAct);

/*@ public normal_behavior

@ requires _timedActs.has(refAct) && _timedActs.has(repAct)

@ && !refAct.getTimedAct().isConcurrent(repAct.getTimedAct());

@ ensures repAct.getPosition() == refAct.getPosition();

@ ensures_redundantly starts(refAct,repAct);

@*/

public /*@model@*/ void makeStarts(TimedActPositioned refAct,

TimedActPositioned repAct);

/*@ public normal_behavior

@ requires _timedActs.has(refAct) && _timedActs.has(repAct)

@ && !refAct.getTimedAct().isConcurrent(repAct.getTimedAct());

@ ensures repAct.getPosition() == refAct.getPosition()

@ && repAct.getTimedAct().getDuration() ==

@ refAct.getTimedAct().getDuration();

@ ensures_redundantly starts(refAct,repAct);

@*/

public /*@model@*/ void makeEquals(TimedActPositioned refAct,

TimedActPositioned repAct);

Figure 11. Specification of methods used to impose a temporal relation of TimedActs of a Course of Actions.

4.5 Animation Specification

Animation is the highest level of abstraction in the model. Users see animations as a simple interval, which can be combined and manipulated to form a new Animation. Animations are built up constructively in the same fashion as Courses of Actions (i.e., Animations are formed by a combination of pairs of Course of Actions and VR Objects or by a combination of Animations). An Animation can represent the behavior of a single object, a group of objects, or all objects of the environment. For instance, consider an application running an animation of all vehicles in a city (e.g., cars, buses, and trucks). One can design one Animation for every vehicle, different Animations for each kind of vehicle, or an Animation with all vehicles in the model. The first option is unmanageable for humans, considering the large number of objects in the environment. The second option gives rise to a reasonable number of entities (Animations) to be manipulated by users on the fly. The last option is the approach used by existing applications and has the disadvantage of limiting users to explore the animation as a whole.

The animation specification (Figure 12) provides a well-known set of model fields to represent the boundaries of the animation interval and methods to create and combine animations by imposing a temporal relation between intervals. Note that there exist two versions of methods to impose temporal relations between intervals: one to combine Course of Actions forming Animations and another to combine Animations forming an even more complex Animation. The specifications of such methods are not presented here but they have the same semantics as the similar set of operations described in the Course of Action specification.

public class Animation {

/*@ public model JMLValueSet _courseOfActions;

@ public model long _start;

@ public model long _end;

@ public model long _duration;

@ …

@*/

public /*@model@*/ void makeMeets(CourseOfActionPositioned refCoa,

CourseOfActionPositioned repCoa);

public /*@model@*/ void makeStarts(CourseOfActionPositioned refCoa,

CourseOfActionPositioned repCoa);

public /*@model@*/ void makeEquals(CourseOfActionPositioned refCoa,

CourseOfActionPositioned repCoa);

…

public /*@model@*/ void makeMeets(Animation refAni, Animation repAni);

public /*@model@*/ void makeStarts(Animation refAni, Animation repAni);

public /*@model@*/ void makeEquals(Animation refAni, Animation repAni);

…

Figure 12. Algebraic specification of Animation.

However, animations have a richer set of methods to combine, manipulate, and define how the animation should be presented. This set of the operations can be divided into three main groups: combinations, manipulation, and presentation operations (Figure 13).

// Combination methods

public /*@ model @*/ Animation intersection (Animation Anim1, Animation Anim2);

public /*@ model @*/ Animation difference(Animation Anim1, Animation Anim2);

public /*@ model @*/ Animation concatenation(Animation Anim1, Animation Anim2);

// Manipulation methods

public /*@ model @*/ Animation scale(Animation Anim1, float factor );

public /*@ model @*/ Animation repeat(Animation Anim1, int repetitions);

public /*@ model @*/ Animation subset(Animation Anim1, long start, long duration);

public /*@ model @*/ Animation move(Animation Anim1, long offset);

public /*@ model @*/ Animation stepwise(Animation Anim1);

// Presentation methods

public /*@ model @*/ void play(Animation Anim1);

public /*@ model @*/ void reverse(Animation Anim1);

Figure 13. Combination, manipulation, and presentation methods of the Animation Specification.

Combination methods produce a new animation through the composition of two animations. The set of combination methods is intersection, difference, concatenation, and union. Methods used to impose a temporal relation between Courses of Actions and Animations can also be considered elements of this set.

· The intersection of two animations generates an animation defined over an interval obtained from the intersection of the intervals used as the arguments of the operation. The result is an animation defined over an interval when only the simultaneous occurrences of both animations will be present. With this operation a user can verify mutual interference between the movement of different objects.

· The difference of two animations generates an animation defined over an interval when the second animation is not defined (i.e., an interval when only the first animation occurs). This operation permits the user to isolate the behavior of the first object during the period when the second object does not occur.

· The union of two animations is a simple combination of two animations while preserving the temporal configuration of individual arguments. This operation is useful to combining animations forming complex animations.

· The concatenation of animations produces a new animation when the second animation follows the first (i.e., the second animation starts immediately after the first). The result is that temporal gaps are eliminated. This operation can be used to analyze the behavior of two objects that have a large temporal separation. This operation is equivalent to performing the makeMeet operation.

Manipulation methods produce a new animation by altering the characteristic of an existing animation. Such manipulations include redefining the animation start point, changing or limiting the duration of the animation, repeating the animation, and turning off the interpolation function. The manipulation operations are scale, repeat, subset, move, and stepwise.

· The scale method changes the duration of the animation interval. The practical effect of the scale method is to change the speed of the animation by slowing down or speeding up a specific sequence.

· The repeat method creates a new animation by concatenating the same animation a certain number of times. Using the concatenation function, the delays specified for the animation are disregarded, implying that the following animation starts as the previous one finishes. The repeat operation is useful to analysts in repeating a critical or complex movement of the phenomenon. This operation can also be used as a combination operation to represent a cyclic movement.

· The subset method extracts a portion of certain animation. The new interval is defined by specifying its start time in the animation space and its duration. All activities outside of such an interval are disregarded. A user willing to analyze critical segments of the animation can use this operation in combination with the repeat operation.

· The move method changes the start point of the animation. This method translates the entire animation by a given value along the animation timeline. This operation has the effect of introducing or eliminating delays in the presentation of the animation.

· The stepwise method turns off all interpolation functions. The animation resulting from this operation presents only the discrete movement of the object, highlighting keyframes of the animation.

Presentation methods are used to present the animation. We have only two methods: play and reverse. Play presents the animation in the order that it was defined, while reverse inverts the order of the presentation.

Combination and manipulation operations have a top-down effect in all entities of the animation model. For instance, considering that we applied the scale operation in a complex animation (i.e., an animation formed by others animations), the duration of all animations, courses of actions, and timed acts are changed proportionally to fit into the new interval. However, the computational cost to perform these operations is minimized by the fact that it is not necessary to verify concurrent changes of attribute types. The entity animation encapsulates the entire behavior of a certain object; therefore, it is impossible to have the same object participating in different animations of a combination operation. The temporal configuration of Timed Acts is invariant under manipulation operations. Thus, Timed Acts that do not compete preserve this characteristic after manipulation operations.

5 CONCLUSIONS AND FUTURE WORKS

We have presented a conceptualization and a formal specification of an animation data model. The modules of the specification represent increasing abstractions of the behavior of objects. At a low level of abstraction, the specification focuses on the description of operations to compose the behavior of an object. These operations are used to coordinate concurrent changes of states and to compose complex behaviors based on temporal relation between intervals. At a high level of abstraction, the specification describes operations to combine, manipulate, and present animations. These sets of operations give an observer the opportunity to explore a virtual dynamic environment, composing your own view of the animated phenomena.

At this point, the animation model deals only with the representation of time-dependent behavior of an object. However, in a virtual exploration of animations interaction becomes also a key issue. The model needs to be extended with operation that represent the behavior of the object in response to some stimulus (i.e., a user action or a specific configuration of the environment).

We also consider important to extent the model to support causality and different representation of the same object. Causal relations are a valuable piece of information that can be used to compose animations. It is important to isolate objects affected by a specific change in the configuration of the environment or objects that lie in a cause-and-effect chain.

Different combinations and manipulations of animations result in different numbers of objects participating in the animation, which can vary from a single object to all moving objects available in the database. When the number of objects participating in the animation increases, concerns about the representation of objects become a key issue for most applications and users. The limitation of hardware does not permit the computation of animations with realistic representations of very objects. Sometimes users prefer iconic representations of objects rather than their realistic representation to analyze and explore their behaviors. Geometric details and realistic texture are hardware-intensive and can easily distract an analysts, but it is extremely useful for the presentation of animations to the general public. Users and applications need operations that change the representation of objects but preserve their behavior.

References

Allen, J. F. (1983) Maintaning Knowledge about Temporal Intervals. Communications of the ACM 26(11): 822-843.

Allen, J. F. and Ferguson, G. (1997) Actions and Events in Interval Temporal Logic. in: O. Stock, (Ed.), Spatial Temporal Reasoning. Kluwer Academic, 205-245.

Arnold, K. and Gosling, J. (1998) The Java Programing Language. Addison-Wesley, Reading, MA.

Astesiano, E. and Kreowski, H.-J. (1999) Algebraic Foundations of Systems Specification. Springer, Berlin.

Dam, A. v., Forsberg, A., Laidlaw, D., LaViola, J., and Simpsom, R. (2000) Immersive VR for Scientific Visualization: A Progress Report. IEEE Computer Graphics and Applications 20(6): 26-52.

Dollner, J. and Hinrichs, K. (1997) Object-Oriented 3D Modeling, Animation and Interaction. Journal of Visualization and Computer Animation 8(1): 33-64.

Elliott, C. and Hudak, P. (1997) Functional Reactive Animation. in: ACM SIGPLAN International Conference on Functional Programming, Amsterdam, The Netherlands, pp. 263-273.

Fiume, E., Tsichritzis, D. and Dami, L. (1987) A Temporal Scripting Language for Object-Oriented Animation. in: Eurographics 1987, Holland, pp. 283-294.

Funge, J., Tu, X. and Terzoupoulos, D. (1999) Cognitive Modeling: Knowledge and Planning for Intelligent Characters. in: Sibgraph'99, Los Angeles, CA, USA, pp. 29-38.

Green, M. and Halliday, S. (1996) A Geometric Modeling and Animation System for Virtual Reality. Communications of the ACM 39(5): 46-53.

Guttag, J. V., Horning, J. J., Garland, S. J., Jones, K. D., Modet, A., and Wing, J. M. (1993) Larch: Languages and Tools for Formal Specifications. Springer-Verlag, New York.

Henriksen, J. (1999) General-Purpose Concurrent and Post-Processed Animation with PROOF. in: P. Farrington, H. Nembhard, T. Sturrock, and G. Evans, (Eds.), 1999 Winter Simulation Conference,, pp. 176-181.

Huisman, M. (2001) Reasoning about Java Programms in Higher Order Logic with PVS and Isabelle. University of Nijmegen, IPA dissertation series 2001-03.

Jacobs, B., Berg, J. v. d., Huisman, M., , M. v. B., Hensel, U., and Tews, H. (1998) Reasoning about classes in Java (preliminary report). in: Object-Oriented Programming, Systems, Languages and Applications (OOPSLA ’98),, pp. 329–340.

Leavens, G., Baker, A. and Ruby, C. (1999) JML: A Notation for Detailed Design. Technical Report.

Leavens, G. T., Baker, A. L. and Ruby, C. (2000a) Preliminary Design of JML: A Behavioral Specification Language for Java. Iowa State University, Department of Computer Science, Ames, Technical Report.

Leavens, G. T., Leino, K. R. M., Poll, E., Ruby, C., and Jacobs, B. (2000b) JML: notations and tools supporting detailed design in Java. Department of Computer Science, Iowa State University, August 2000, Technical Report.

Lee, G. S. (1998) A General Specification for Scene Animation. in: International Symposium on Computer Graphics, Image Processing, and Vision - Sibgrapi'98, Rio de Janeiro, Brazil, pp. 1-8.

Little, T. D. C. and Ghafoor, A. (1993) Interval-Based Conceptual Models for Time-Dependent Multimedia Data. IEEE Transactions on Knowledge and Data Engineering (Special Issue on Multimedia Information System) 5(4): 551-563.

Luttermann, H. and Grauer, M. (1999) VRML History: Storing And Browsing Temporal 3D-Worlds. in: ACM Fourth Symposium on VRML, Paderborn, Germany, pp. 150-163.

MacEachren, A., Edsall, R., Haug, D., Baxter, R., Otto, G., Masters, R., Fuhrman, S., and Quan, L. (1999) Virtual Environments for Geographic Visualization: Potential and Challenges. in: Proceedings of the workshop on new paradigms in information visualization and manipulation, Kansas City, MO USA, pp. 35-40.

Mallgren, W. R. (1982) Formal Specification of Interactive Graphics Programming Languages. The MIT Press, Cambridge, Massachusetts.

Manoharan, T., Taylor, H. and Gardiner, P. (2002) A Collaborative Analysis Tool for Visualization and Interaction with Spatial Data. in: 7th International Conference on 3D Web Technology - Web3D'02, Tempre, Arizona, USA, pp. 75-83.

Najork, M. and Brown, M. (1995) Obliq-3D: A High-Level, Fast-Turnaround 3D Animation System. IEEE Transactions on Visualization and Computer Graphics 1(2): 175-193.

Raper, J. (2000) Multidimensional Geographic Information. Taylor & Francis, London.

Strauss, P. and Carey, R. (1992) An Object-Oriented Graphics Toolkit. Computer Graphics 26(2): 341-349.

Varzirgiannis, M. and Sellis, T. (1996) Event and Action Representation and Composition for Multimedia Application Scenario Modelling. Athens.

Weiss, R., Duda, A. and Gifford, D. (1995) Composition and Search with a Video Algebra. IEEE Multimedia 2(1): 12-25.

Wing, J. M. (1987) Writing Larch Interface Language Specification. ACM Transactions on Programming Languages and Systems 9(1): 1-24.

Zeleznik, R., Conner, D., Wloka, M., Aliaga, D., Huang, N., Hubbard, P., Knep, B., Kaufman, H., Hughes, J., and Dam, A. v. (1991) An Object-Oriented Framework for Integration of Interactive Animation Techniques. Computer Graphics 25(4): 105-112.