 |
Boris van Schooten
Parlevink group,
Faculty of Computer Science
University of Twente,
Enschede,
P.O. Box 217, 7500 AE, Netherlands
schooten@cs.utwente.nl
http://wwwhome.cs.utwente.nl/~ schooten/vetk/
Complex applications such as multi-user applications may fruitfully be viewed as being composed of a number of independent agents which access and modify a shared data structure. We will view this shared data so as to include the domain data being viewed and edited as well as the entire user interface state.
Such a shared data concept may be effectively modelled using database techniques. One of the aspects of such modelling is the specification of requirements on the structure and evolution of this shared data. This may enable a desirable level of abstraction from the implementation of the user interface. Such a specification may be used to check the correctness of a given agent or ensemble of agents working on this shared data. To enable such checking, a formal coupling between the requirements and the executable system is desirable.
This paper proposes a constraint specification language, providing formal versions of traditional UML-type structure diagrams and statecharts, in combination with arbitrary constraints, which are similar to Object Constraint Language (OCL) specifications. These are coupled to applications written in a multi-user toolkit by means of code assertions. The usefulness of this specification technique is assessed by means of specification of a small multi-user application.
In this paper, we will address system design issues of complex interactive systems, such as multi-user systems. We will view an interactive application as consisting of a number of separate (that is, concurrent, or at least, independent) agents that access and modify shared data. With shared data we mean both domain data (the data being viewed and edited) and user interface data (presence of windows, positions of scrollbars, item selections, etc.).
Such a concept of shared data is central to many user interface modelling techniques, though emphasis is usually laid on domain data. One of the goals of architectural styles [4], for example, is to identify and compartmentalise this data, and restrict and clarify its access by means of architectural constructs and interface definitions. For example, in the MVC architectural style [9], one splits the shared data into a number of Model objects, and specifies the interface of each Model object separately. In the PAC style [9], an additional architectural constraint is prescribed that limits access to compartments by means of an encapsulation hierarchy.
Such models assume that the data can be fruitfully separated into a number of relatively isolated compartments. However, in many practical cases, there are complex queries and operations that need to be done on the data. These go beyond that of single compartment that is only accessed by a limited number of agents. For example, in systems providing inter-user awareness such as What You See Is What I See (WYSIWIS) [16], the user interface data of one user (such as scrollbar and mouse cursor positions) is concurrently accessed by different users in different ways, in order to enable the users to see each other's activities. Another example are multimodal systems and personal assistant agents, which typically operate by tracking the activities of the user in different parts of the user interface.
In some multi-user toolkits we already find that the different user applications interact by accessing a single global shared data structure [13]. Here, we go a step further, and use a database approach for the modelling of all shared data [17]. An important aspect of specifying a system based on such a shared data model is describing global properties of this data. In this paper, we will discuss how formal versions of structure diagrams, finite-state machines, and other types of constraints may be combined to formally specify global properties of an application's shared data in a declarative manner. We propose a new language for describing these models and show how an application can be specified using this manner of specification.
The paper will be structured as follows. First, we will discuss existing efforts on constraint specifications, and their relation with this work. Then, we will describe the constraint language itself, and how it is coupled with a working application. The language will then be assessed by means of an example specification, and its potential will be discussed.
Many formal languages exist that are suitable for defining constraints on data, though the means they provide for coupling to executable systems vary. A proper coupling with the executable system would however benefit the practical usefulness of such a language. A recent attempt at standardisation and stimulation of wide acceptance of such constraint specifications is OMG's Object Constraint Language (OCL) proposal [1]. OCL is a practical language that is specially designed to be easily executable. Basically, OCL provides straightforward correctness assertions in the form of truth expressions over sets and other collections, using quantifiers. These collections are defined by means of `database' queries, with the collections being the queries' results. This combination of assertions and queries provides a means to specify structural constraints.
OCL's query facilities basically consist of navigational expressions, which enable navigation through object structures by following references. Note that this bypasses the encapsulation principle as prescribed by object-oriented design. In this regard, OCL's manner of specification is database-oriented rather than object-oriented. An OCL-like language could fruitfully be used to describe a system based on database concepts.
Some compilers exist that couple OCL to executable code, with the most notable one being the Dresden compiler [10]. It enables OCL constraints to be added to Java classes using concise annotations which generate extra code when compiled.
Another language that combines structure-based specifications with assertions is the Alloy language [2]. Though Alloy enables model checking, it provides no easy coupling with a full executable system.
Various efforts have been made to employ traditional abstract models such as structure diagrams and finite-state models for interactive software. While such (typically diagrammatic) specifications are not necessarily formal, they may for example be formalised by translation into an OCL-type language.
Structure diagrams, such as entity-relationship diagrams (ERDs) and UML's class diagrams [3,6] are well-used. Many (CASE) tools exist that couple such specifications to executable code, for example by means of generation of code skeletons [11]. Usually though, these specifications are primarily used to describe the domain, and not the user interface. However, informal usability methods such as ERMIA [3] have shown that they may prove quite useful for describing usability aspects of user interfaces as well.
Many models exist that specify the behaviour of a user interface using some form of finite-state machines. Finite-state machines and their many variants are generally intuitive and easily executable, may be coupled to sequence specifications, such as usage scenarios [18], and may carry all the way into a full system [15,8]. However, they are limited in their expressiveness because they can only practically describe a very limited number of states, requiring a large (and heuristic) abstraction step to be made with respect to the executable system. In the well-known statechart model [7], transitions are specified by means of truth expressions, enabling such an abstraction step. UML 1.4 [6] specifies that a statechart corresponds to the behaviour of an object in a structure diagram. Various development environments exist that combine state machines with structure diagrams in a similar manner [11,12].
There are much fewer models that integrate state machines, structure diagrams, assertions, and executable code, in such a manner that the correspondence between them is easy to understand and the formal coupling between them is ensured. In UML, there are plans to formally integrate structure diagrams and statecharts with OCL. The Teallach environment [5] provides both diagram notations, and enables OCL expressions to be used in some places. Still, there is little experience with using such combined specifications in interactive systems.
In this section, we describe a constraint language that enables constraints on shared data to be specified. The language enables OCL-type assertions, and has special notations for description of entity-relationship constraints and state machines. A code module may be generated from a specification, which may be added to a running system to provide diagnostic information, such as state transitions and constraint violations. The language provides a visual representation, with a comprehensive mapping of statements in the language to structure and state diagrams. Currently, there is no graphical tool for editing specifications, and diagrams are instead generated from the textual specification using a graph layout tool.
It is convenient to use a programming language or toolkit that is easily mappable to data structure constraint specifications. For this purpose, we use the VETk system [17], which models all shared data (which includes user interface state, even including mouse clicks and movements) using a special low-overhead relational database. Since everything is modelled as database accesses, the mapping between the constraint specifications and the executable code is quite close. Since this system already provides database queries as a basic construct, we get query facilities for free. Additionally, it provides a publish-subscribe model, which makes the tracking of changes made to the database easy.
Mapping of basic structure diagrams is relatively straightforward: one just defines a mapping between entities, relations, and attributes as defined in the constraint language with those in the database. This mapping is used to check relational multiplicities.
Mapping of state machines is more problematic however. The necessary abstraction step between the concrete state of the system and the abstract state machine should be formal, yet it should allow proper flexibility. Following Harel's statechart approach [7], we specify transitions by an event, a condition on the state of the system, or a combination of both. Events and conditions may be specified as arbitrary OCL-type truth expressions.
Unlike OCL, our language separates the definition of the sets (by means of queries), and the constraints on them. First, we will explain how sets are defined, then we will describe the constraint language.
A set is defined by means of a query. The contents of a set at a specific moment in time is the result of this query at that specific moment. Queries are written in Prolog style. Database tuples (i.e. entities and relationships) are specified in the form:
<tuplename> `(' ListOf[ <field> ] `)'
Fields (which represent attributes or references) may be literal values, such as integers, strings, or database keys. In queries, they may also be variables: the tuple then specifies a search pattern in which the variable is a free variable. In our constraint language, queries are of the form:
`set' <setname> `(' ListOf[ <variable> ] `)'
`:' SequenceOf[ <tuple> ]
The right hand side (the clause after the colon) specifies the query pattern. The pattern's query result is a set of bindings of the free variables found in the tuples. For each binding, those variables are taken that are listed in the left hand side. This results in a set of tuples: the query result. Here is an example taken from the card game specified below:
set userselected(~player,~card) :
selected(~player,~card) participant(~player,self,_)
The set that we specify here is a set of 2-tuples called userselected. This stands for the cards that are selected by each of the players (indicated by the relation selected(~ player,~ card)) which participate in a specific game (indicated by the relation participant(~ player,self,_)). Note that the identifiers which start with a tilde ~ symbol indicate variables. The identifier self indicates a constant. In fact, self is a special constant that stands for the entity that the set is defined in, in this case the entity card. Finally, note the underscore _ symbol, which is a wildcard that denotes that the value at that position does not matter.
It is these query specifications that are used to provide query facilities to the OCL-type expressions found in our language. They are in some ways more powerful than OCL navigational expressions, because they enable Prolog-style pattern matching. If we do not consider efficiency and ease of implementation, there is no reason why even more powerful query facilities might not be added to any OCL-type language.
Now, we will continue with the specification language. The structure specifications are basically entity-relationship models. One may define entities and relationships in the following way:
[ `entity' | `relation' ] `('
ListOf[ <attribute> | <entity> `:' <multiplicity> ]
`)' `{'
<values and events>
<sets>
<statemachines>
<assertions>
`}'
An entity or relation may have attributes, and may have references to any number of entities, in which case the multiplicity of each reference is specified. Note that entities too may directly refer to other entities. While this practice is often considered too implementation-oriented, at least the designer does have the ability to specify this if desired. An entity or relation has a body, which specifies attributes that are optional (called values) and operations (called events).
Other constraints may also be specified as properties of the entity or relation. These are general assertions and state machine specifications.
The state machines that may be specified are basic finite-state machines, with the difference that a transition may be specified by two arbitrary truth expressions: one specifies an event, and the other a state condition. A transition occurs when the state condition is true and the event occurs (i.e. the condition specified by its truth expression goes from false to true). Either event or condition may be left empty. A state machine is specified by:
`statemachine' `{'
SequenceOf[
<sourcestate> `->' <destinationstate>
`{' <event> `}' `{' <condition> `}'
]
'}'
Assertions may be specified inside an entity's or relation's body, or as separate statements. Assertions are of the format:
`assert' OptionalListOf[ <state> ] `{' <assertion> `}'
In case we specify one ore more states, the assertion only has to hold when the entity in which the assertion is stated is in one of those specific states.
The events, conditions, and assertions are OCL-like truth expressions. The expressions have the following form:
`exists' `(' <setexpression> `)'
| `forall' `(' <setexpression> `)'
| <setexpression>
| `size' `(' <setname> `)' <comparison_op> <value>
| <expr1> [ `and' | `or' ] <expr2>
| `not' <expr>
With the exists and forall quantifiers, the specified setexpression is evaluated for each combination of elements in each of the sets mentioned in the expression. In case of exists, the result is true as soon as one of the expressions results in true. In case of forall, the result is true if all of the expressions result in true. Specifying just a setexpression is equivalent to using an exists quantifier. The size operator counts the number of elements in a set. Finally, we may combine any of the above expressions using the Boolean operators and, or, and not. Setexpressions are Boolean expressions in which individual fields of previously-declared sets may be addressed using the notation setname.fieldname.
Here are some examples of truth expressions:
not userselected
/* true if and only if userselected is the empty set */
forall(userselected.player != ForbiddenUser)
/* becomes false if the user ForbiddenUser selects a card */
size(userselected) <= 3
/* true as long as userselected contains <= 3 elements */
player.joined==0
/* true when there is at least one player with joined = 0 */
Though a more thorough evaluation would be desirable, at this stage of research we will begin with a small assessment of the language using an example application. The application we will assess this specification language with is a multi-user card game, a computer version of the game of Set. A working implementation of this application already existed. Usually, one would start specifying the constraints much earlier in development, but such methodological issues, that is, when to specify what, will not be considered here.
The suitability of the constraint language will be assessed in the following manner:
The example application is implemented using the following agents: a game agent incorporating the game rules, and standard agents corresponding to the user interface objects: buttons, textfields, textareas, lists, and canvases. First we will give a natural-language specification of the application. Then we will give the constraint specification (figure 4) and the corresponding diagrams. Figure 1 shows a structure diagram of the system, figure 2 and 3 the state diagrams of the game and user.
Natural language specification. Users are able to log in via the Web, after which they are presented with the game window. Here, they can fill in their name, create and delete games, or join games that have not yet begun. When a game is joined, the user can talk to the other users that have joined the game. Once a game is started, the cards being played with are displayed. The game proceeds as follows: 12 cards are laid out from the deck on the table. Now, the players have to search for combinations of three cards that satisfy certain criteria; such a combination is called a `set'. The first one to see a set calls `set!' and then has a couple of seconds to point out the three cards. These are removed and replaced with cards from the deck. The game continues until the deck is exhausted. The player with most sets wins. When no player can find any sets, extra cards may be laid out. The game should also have the option to point out sets. This pauses the game, and enabling all players to see the sets on the table, after which the game may be continued with fresh cards.
The process of specification was found to improve insight in the application, as several changes were made to the design of the system that were prompted by insights made from the constraint specification. Assertion violation detection helped in adjusting the specification and the implementation to each other.
The program was originally developed with help of an informally-specified structure diagram specified in the earliest phases of development, which was found very useful. The formal structure diagram was however more complete and accurate. From this formal diagram, it became clear that a redundant relation was present, and that some of the references were implicit. These deficiencies were easily corrected.
Initial specification of the state machine for the game showed that the different modes that the game could be in were not very well modelled. In fact, some illegal user actions were possible under some conditions, such as selecting cards when the player did not call `Set' first. After specification of the state machine and the corresponding assertions for each state, the conditions under which user actions were available or not were made quite clear. Also, it became clear that some transitions were possible that were not thought of at first, such as the transition from Playing to Watching.
While the general specification techniques used are relatively traditional, the subject and focus of the specification is relatively unusual. In this example, it resulted in a simple, straightforward specification that nevertheless covers an interesting part of the application. The approach provides a level of abstraction that may also be suitable for describing an abstract user interface model which may be filled in by alternative concrete user interfaces [14].
The close coupling of the specification with the executable system provided some extra insight, showing that such a coupling is indeed useful. Some discrepancies of previous informal specifications with the system were clarified and some failed assertion checks and state transitions uncovered further errors. Still, the resulting structure and state diagrams are relatively easy to read, and could effectively be used as part of usability specifications. The notation could provide a formal bridge between usability methods and the implementation.
The structure diagram makes quite clear how agents should access their required data. For example, if we want the users to be able to view a list of participants, they can just query the participant relations. If we want users to become aware of the cards that another user is selecting, we can simply query the selected relations. This structure specification is similar in spirit to ERMIA specifications, and can be used to decide on usability issues, such as which entities and relations should be visible to the users.
The state diagrams contributed to intuitive insight, but they could be more than just part of the constraint specification. They may be useful as part of the specification of the executable system itself. Once the state machines were specified, there was often the desire to read out their state from within the application. This is not exactly surprising, as much of the systems' behaviour can be effectively expressed in terms of these states.
This document was generated using the LaTeX2HTML translator Version 2K.1beta (1.47)
Copyright © 1993, 1994, 1995, 1996,
Nikos Drakos,
Computer Based Learning Unit, University of Leeds.
Copyright © 1997, 1998, 1999,
Ross Moore,
Mathematics Department, Macquarie University, Sydney.
The command line arguments were:
latex2html -split 0 -show_section_numbers dsvis02-schooten-final.tex
The translation was initiated by Boris van Schooten on 2002-09-10
