Formal Specification of Human-Computer Interaction by Graph Grammars under Consideration of

Formal Specification of Human-Computer Interaction by Graph Grammars under Consideration of Information ResourcesBettina Eva SucrowData Management Systems and Knowledge RepresentationDept.of Mathematics and Computer ScienceUniversity of Essen,45117Essen,Germanysucrow@informatik.uni-essen.deAbstractA successful design of an interactive system requires aclear understanding of human-machine interaction.For thespecification of such a system a precise consideration ofthe user’s context during each step of the development pro-cess is therefore necessary.Moreover,a formal specifica-tion method for expressing interaction is highly desirablein order to achieve a precise and continuous specificationprocess between the requirements and design stages.In this paper1several of the environmental cues influenc-ing the user during the interaction with a system are con-sidered.These environmental cues are modelled using theconcept of information resources.Interaction is describedusing these resources and formally specified by the notationof graph grammars in order to be able to reason about asystem,to assess a system wrt important properties and,finally,to achieve a continuous specification process be-tween the requirements and design stages.This approachwill be demonstrated by specifying a safety-critical systemconcerning the interaction between the pilot and theflightmanagement system on theflight deck of an aircraft.1.IntroductionWell designed interactive systems presuppose a deep un-derstanding of the interaction between man and machine.According to[17]and[2]such an understanding can beachieved by considering the user’s context,that is all theenvironmental cues influencing him perpetually during theinteraction with a system.Such environmental cues includeconstructs that may be part of the user’s internal cognitiveprocessing such as plans and goals or may be externally rep-the formalism of graph grammars is used in[6].Dialog states describing user interface objects with their current appearance and their respective relationship to the underly-ing application are formally specified by directed attributed graphs.Transformations of one dialog state into another one by an event(raised by the system’s or the user’s side) are formally specified by graph rewrite rules.In[12]this approach has been used in order to formalize the control window of a part of a complex real system by graph gram-mars(see also[15]).This system consists of a library of numeric progam packages for solving non-linear equation systems and the correct and comprehensive specification led to a far better interaction process.[16]shows an approach for integrating software-ergonomic aspects in formal speci-fications of graphical user interfaces using graph grammars in order to improve human-machine interaction.Although approaches of specifying graphical user inter-faces by the formalism of graph grammars provide expres-sive as well as understandable specifications the considera-tion of graphical user interface objects with their relation-ships to the underlying application and the task-oriented view are not sufficient for the aim of modelling interaction between humans and complex systems in a suitable way.In this paper interaction will be modelled in terms of in-formation resources and the formalism of graph grammars will be used to specify human-machine interaction formally. The interconnection of the various resources will be speci-fied by graphs and the mechanism by which these connec-tions are transformed as the interaction progresses will be specified by graph rewrite rules.A graph grammar specifi-cation of this kind will allow the reasoning about a system, the assessment wrt important properties and a consistent re-finement into a more concrete specification.First,we introduce the formal notation of graph gram-mars and demonstrate by a small and simple example how they could be used to specify a graphical user interface.In order to express human-machine interaction under the con-sideration of environmental cues influencing the user during the interaction with a system we then briefly introduce the concept of information resources.Based on these prepara-tions we explain how interaction can be expressed in terms of information resources and specified formally by graph grammars.This is demonstrated by specifying a safety-critical system concerning the interaction between the pilot and theflight management system on theflight deck of an aircraft at a still abstract stage.Moreover,it can be proved already at that abstract stage whether some important prop-erties are fulfilled by that specification or not.Further,in order to refine that stage into a more concrete specification a part of a graph grammar at a meta level is constructed.A graph grammar of this kind will allow,finally,to achieve a continuous specification process between the requirements and design stages.2.Specification by Graph GrammarsGraph grammars represent a highly suitable formalism for specifying statics and dynamics of interactive systems. Graphs describe states,graph rewrite rules describe changes of states in a powerful but understandable manner.It follows a very brief account of the formal definitions for the graph grammar formalism for the sake of under-standability.Sometimes the definitions will be only semi-formal and incomplete due to lack of space.We therefore refer to[13]for a detailed and complete description.2.1.The Graph Grammar FormalismLet and be two type variables denoting types for labelling nodes and edges of graphs respectively. The sets used to actualize and are not neces-sarily simpleflat alphabets,but could also be sets of func-tions,relations,etc.as attributes.We define:Definition An-graph is a system,whereset of nodes,set of edges,source function of edges,target function of edges,node labelling,edge labelling.represents a directed node and edge labelled graph. For describing modifications of graphs by graph rewrite rules we need the definition of a match between two graphs: Definition A graph match of a-graph in a-graph is given by a4-tupel,whereand mappings,node at-tribute match predicate,edge attribute match predicate.For the induced match it has to be assured on the one hand that and map consistently the source and target of each edge in graph onto nodes in the target graph such that the graph structure of -i.e.without considering labels-is mapped ontoa proper subgraph of.On the other hand the labelof a graph element(node or edge)in and the label of the corresponding picture of that graph element in graph(under the mapping or respectively) have to be compatible with respect to the predicates or respectively.Modifications of graphs are described by graph rewrite rules:Definition A graph rewrite rule is a tripel of graphs,where graph is the left hand side of the rule, graph is the right hand side of the rule and graphis the so called glueing graph.takes care that no dangling edges appear in the new graph after apply-ing to the old graph(see also the definition below).Hence,identifies some anchor elements which have to remain unchanged by the modification and is a sub-graph of and as well.Definition A modification of a graph into a new graph by applying a graph rewrite rule is realized by the following two principal steps:1)a graph match is chosen between the graph andthe graph to be modified,2)the induced match of graph is removed in graphand graph is added.The connection of graph to the remaining part of graph is given by the glueing graph(see above).At this point we have all necessary preliminaries to define: Definition A graph grammar is a system,where,are node and edge attributes respec-tively,is a set of graph rewrite rules,is a set of attribute match predicates required for a graph match,is the start graph(is a()-graph). For the sake of simplicity a graph grammar will be de-scribed in the following by,where denotes the start graph and the set of graph rewrite rules.Definition A graph grammar language is the set of all graphs generated by a graph grammar.In the next section we demonstrate by a simple example how graph grammars can be used to specify graphical user interfaces.This is done in preparation for using this for-malism in order to specify interaction modelled in terms of information resources.2.2.Specification of Graphical User InterfacesThe idea to describe graphical user interfaces by graph grammars is inspired by the observation that a graphical user interface can be characterized by dialog states and dia-log state transitions(for a more detailed description cf.[6]).A dialog state describes the appearance of the user in-terface objects of an application and the relationships be-tween them in a particular situation.It can be formally specified by a directed attributed graph.The nodes rep-resent graphical user interface objects,attributes attached to the nodes specify resource values(er interface-as well as application-specific informations)of the respective objects.The edges of the graph represent the specific rela-tionships between the objects.Attribute wh,e.g.,indicates the widget hierarchy.While relationships of this kind re-fer to the human-machine interface,there exist other ones refering to the representation of the data and operations of the underlying application.The latter case is handled more deeply in[5]where the main emphasis lies in investigating the various interdependencies which possibly exist between the functional kernel of an interactive system and its human-machine interface with the goal offinding suitable software components within an architectural structure of the system.A dialog transition is a possibly complex transformation of a dialog state into another one caused by an interaction between the system and the user or by the system.It can be formally specified by a graph rewrite rule.The following simple example demonstrates this ap-proach.Suppose,one can start a system which opens a sim-ple listbox with one item.One can delete this item and then finish the system,provided that the item does not exist any-more.The two states and before and after deletion of the item are sketched below together with their corresponding graphs and.ListWinListboxS StartG Empty ListWinListboxS EmptyGraph rewrite rules,,specifying the three user interactions causing the transitions between the states are sketched below.Here,the states before start-ing and afterfinishing the system are specified by the empty graph.It is denoted by and graphically indicated by.∅ListWinListboxP Start= (G StartG0,,G0)::=ListWinListboxListWinListboxP Empty= (G Start G Empty,,G0)∅::=P Stop= (G Empty,,G0)G0 In this way the simple listbox system is specified by the Graph Grammar whereStart Graph,set of Rewrite Rules.Graph grammar specifications of this kind are very suit-able for designing or redesigning graphical user interfaces for already existing applications.However,for a deep understanding of human-machine interaction in order to achieve suitable specifications of interactive systems a pre-cise consideration of the user’s context is highly necessary.3.Specification of Interaction Using Informa-tion ResourcesInteraction can be modelled based on the concept of information resources(more deeply handled in[17],[2]). This idea is influenced by the approach of distributed cog-nition[7]which sees resources as distributed across com-ponents of the whole system.Several of the environmental cues influencing the user during the interaction with a sys-tem are captured by information resources.Such informa-tion resources include plans,goals,world state,interaction history,action-effects and action-affordances.They may be part of the user’s internal cognitive processing or may be externally represented in terms of other artefacts.A goal, for example,may be in the user’s head,but could also be represented in a specific state of an interactive system by a specific graphical user interface object on the screen.In this way,information resources can be represented internally or externally and canfind different expressions when repre-sented externally.The distribution of these resources and the properties of their expressions are what shape interac-tion([17]).The user tries to achieve goals by interacting with a sys-tem and he has plans in his head during certain time periods to achieve these goals.Action-affordances refer to the set of possible next actions that can be taken,given the current state of the system.An action-effect mapping is a state-ment of the effect that an action will have if it is carried out.Such information resources are highly suitable criteria for getting an understanding of interaction.But there does not exist any formal specification of human-machine inter-action modelled in terms of information resources.In the next section it will be explained how information resources can be used to model interaction and how this can be specified formally by graph grammars.This approach will be demonstrated by an example in the second section where the interaction between the pilot and theflight man-agement system on theflight deck of an aircraft will be con-sidered.3.1.PhilosophyDescribing interaction in terms of information resources and specifying this formally by graph grammars gives a suitable insight into the system’s and the user’s side at the same time in every state.Suppose,in a current state of in-teraction the user has a goal in his mind he would like to achieve by interacting with the system.This goal is not yet completed but is reflected in a part of the system’s user in-terface in some way.This could be,for example,a certain button with a corresponding meaning,or a textfield which already suggests a corresponding input,or the like.In such situations the user understands the action he could perform to complete the goal as well as the effect that action would have if it is carried out.In this model of interaction in the current state several information resources are involved:the goal internally rep-resented in the user’s head as well as externally in a part of the system’s user interface;the action-affordance referring to clicking a button or typing into a textfield;the action-effect referring to the completion of the goal;the history of state indicating that the goal has not yet been completed.This state of the interaction can be formally specified now by a suitable graph.To demonstrate this a small part of the example described more concretely in the next section will already be used.The goal Fly offlying an aircraft can be completed by performing the action<a>within the subpart Fl of the system’s user interface.The value of the boolean attribute done specifies that the goal Fly has not yet been com-pleted.Note,that all parts of this specification,action<a>, goal Fly and the corresponding subpart Fl are still speci-fied in a highly abstract manner.At a more concrete stage of specification they would be much more refined.As will be seen also in the next section goals as well as subparts of the system’s user interface are specified by nodes of corresponding types respectively.Different shapes of nodes denote different types of nodes.The composition of goals into subgoals is specified by directed edges of type goal hierarchy(see below).Analogously,the subparts of the system’s user interface are related to each other by di-rected edges of type widget hierarchy.The relationships be-tween the user’s goals and the subparts of the system’s user interface are captured by edges specifying the various possi-ble relationships between them according to the distributed information recources.For the action-effect mapping that means:if a goal may be completed or at least approached by the effect of an action within a subpart of the system’s user interface then a directed(dotted)edge labelled by that action will lead from that user interface part to the corre-sponding goal.Action-affordances,the actions offered by a system in a current state are specified by the collection of actions attached to all the action-effect edges appearing in the graph specifying that state.History may be specified bya boolean attribute attached to a goal node indicating that this goal has not yet or already been completed.In more complex cases a counter may be introduced by which his-tory can be specified more precisely.Graph rewrite rules specify the dynamics of the system,the interaction.Every rule contains within the graph on its left hand side exactly one action-effect edge.The left hand side specifies the conditions under which the correspond-ing action may be performed.The right hand side specifies the changes that will take place by applying that rule.The following rule gives an impression of this mechanism.::=The left hand side of this rule matches a graph under the condition that the boolean attribute done attached to the goal node Fly has the value false indicating that this goal has not yet been completed.If the left hand side of the rule matches then it will be substituted by its right hand side.By applying this rule a change of the value of the attribute done into true will be performed indicating that the goal Fly has been completed now.3.2.Example:Interaction between the Pilot and theFMSA safety-critical system,the interaction between the pilot and the flight management system (FMS)on the flight deck of an aircraft will be considered.First,a specification of the interaction at a still abstract level will be presented.Subsequently,some claims concerning the validity of important requirements and certain helpful properties are proved.This shows that it is possible to perform an assessment of the design already at this early stage of specification.Especially,the requirement concerning a deliberate confirmation of a specific mode change by the pilot will be considered.A requirement of this kind is important for increasing the chance to prevent mode errors.Errors of this kind have led already to accidents demanding victims (cf.[10],[11]).SpecificationThe specification captures the entire interaction required to tackle the stages beginning with the take-off and ending up with the landing.The first state of the entire interaction may be specified by the start graph below (the pictures de-noted by Pilot and FMS are depicted due to orientation).The root node on the pilot side specifies the top level goal TLG with the meaning of a special flight.This goal is de-composed into the three subgoals Start ,Fly and Land ,landing again is decomposed into the subgoals CNM (chang-ing the navigation mode),EDI (entering the descent input)PilotF M Sand TD (touch down).All goals not further decomposed are associated to subparts of the system’s user interface on the FMS side.Action-effect edges indicate that actions of type <a>could be performed within parts of the system’s user interface in order to complete the respective goals.In the autopilot system the modes of the navigation and descent are automatically coupled (cf.[10]).For that reason the corresponding parts of the system’s user interface at this stage can already be grouped together by specifying them,e.g.,as subwidgets of a and Ed are ex-amples for such subwidgets witha common superwidget U .Moreover,because of the importance of the actual modesof Cn and Ed in every situation a node of a new type denoted by a different shape is introduced.It has an attribute indi-cating the current mode value of its associated system part,e.g.mode value TRK for Cn ,and a specific edge connects this mode node with its respective user interface part.Graph rewrite rules specify the interactions.The first rule specifies the start of the flight.::=P Start:This rule matches under the condition that the goal Start has not yet been completed as indicated by thevalue false ofthe attribute done on the left hand side ofthe rule.In the case of amatch the left hand side of the rule will be substituted by its right hand side.This specifies that the ac-tion <a>performed within the user interface part St leads to the completion of the goal Start as indicated by the value true of the attribute done on the right hand side of the rule.The next rule specifies the flying stage.P Fly:::=This rule matches under the condition that the goal Start has already been completed but the goal Fly has not yet been completed,and it works analogously to the previous rule.The next rule specifying the changing of the navigation mode applies under the condition that the goal Fly has already been completed.P CNM :::=This rule changes the value of the navigation mode fromTRK to HDG (Track to Heading )as can be observed by the mode node connected to the related subpart Cn of the sys-tem’s user interface.Such a change is sometimes necessary in order to comply with radar guidance ([10]).But addition-ally,the rule does something else.A new goal Confirm!appears with related user interface part C within which an action <conf>can be performed to complete this goal.One can imagine C as a modal subdialog or a dialogbox.The goal Confirm!is added here in order to force the pi-lot to confirm the change of the descent mode from FPA to V/S (Flight Path Angle to Vertical Speed )which is automat-ically coupled with the change of the navigation mode from TRK to HDG .This is indicated to the pilot by the value of the attribute val attached to the node C .Now the specification has to assure that the pilot indeed can not do anything else except this confirmation.There-fore,the boolean attribute modeflag is attached to the goal node Land .Its value is always true except in the sit-uation that the pilot changes the navigation mode where its value becomes false .This can be seen by comparing leftand right hand side of the rule.If the modeflag is false in the current state graph then only one specific rule matches,namely the following one specifying the ex-pected confirmation by the pilot as well as the automati-cally coupled change of the descent mode.The right hand side of the rule shows that after its application the value of Land.modeflag is true again and that the subgraph con-taining the goal Confirm!has disappeared again.P Confirm :::=The penultimative rule specifies theentering of the de-scent input which is a subgoal ofthe landing stageand is therefore performed under the condition that the goal Flyhas already been completed.P EDI:::=Finally,the last subgoal of the landing stage,the touchdown goal,is specified by the following rule applicable un-der the condition that the entering of the descentinput has already been completed.PTD:::=This rule,finally,completes the entire top level goal,the special flight.Therefore its right hand side consists only of the goal node TLG and the value true of the attribute done indicates that TLG has been completed now.Despite existing techniques in the theory of graph gram-mars for aggregating set of rules differing only in the la-bels of their graphs (cf.[4])two further rules andare added specifying the change of the navigationand descent modes also in the other direction,from HDG to TRK (Heading to Track )and from V/S to FPA (Vertical Speed to Flight Path Angle )respectively.Thus,the inter-action between the pilot and the FMS can be specified at a still very abstract level by theGraph GrammarwhereStart Graph,.This specification allows to prove some properties and requirements already at that abstract stage.AssessmentWhen designing a dynamic system it is highly important to be able to prove already at early specification stages that certain actions take place before or after other ones.Hence,the first claim concerns the required order in which the three goals Start ,Fly and Land are intended to be completed.Claim1:The goals Start ,Fly and Land will by all means be completed in the required order!Proofonly matches graphs of the kind wherewithc)All rules contributing to the completion of goal Landare only applicable if goal Fly has been completed!This has to be shown for all rules in the set:The proofs for and work analogously to proof1b).is only applicable directly af-ter(because of the attribute).is only applicable after(because of the at-tribute)One very important requirement is to assure that the pilot is always aware of the actual mode values.Claim2:Any indirect(caused by another action)change of the descent mode will be performed through confirmation by the pilot!ProofA switch between the two navigation modes TRK and HDG is specified by the two rules and re-spectively.Both work under the conditionaccording to proof1b).A specification describing the interaction between the pilot and the FMS at an abstract level has been constructed so far. Further,some important requirements could proved to be true already at this abstract specification stage.In the next chapter it will be investigated how such an abstract specifi-cation could be refined continuously.4.Refinement:Graph Grammar at a MetaLevelIn order to refine the specification of the interaction be-tween the pilot and the FMS the start graph in section3.2 has to be considered again.Modes are specified already but they are not visualized to the pilot who has to be aware of their values in every situation to increase safety for the flight.An idea in order to refine this specification wrt to mode visualization is to apply a graph rewrite rule at a cer-tain meta level.Such a rule extending the state graph wrt to mode visualization could look like the following.::=The left hand side matches whenever a system’s user in-terface part is connected to a mode node by a respective edge.The free variable W indicates that application of the rule is possible wrt any system part under the conditions specified by the left hand side of the rule.The same holds for the value of the current mode indicated by the free vari-able MV.Substitution by the right hand side of the rule im-plies an extension wrt the required mode visualization.An additional system part denoted by the free variable SW will be created by which the current mode value MV becomes visualized.One can think about this new part as a label with a bright background colour or the like.The fact of visual-ization is explicitly specified by a directed edge labelled by the constant attribute vis and leading from the mode node M to the node SW describing the new system part.Application of the meta rule to the state graph in section 3.2would lead to the following state graph where the visu-alization of the navigation as well as of the descent mode is specified.The visualization of the two modes is realized by the new user interface parts SC and SE respectively.Pilot F M S The aim is to apply such a meta rule to all occurrences of its left hand side in the graph grammar specification of an interactive system according to the result of the communi-cation between designer and customer.The meta rule will belong to a graph grammar at a certain meta level.This graph grammar has to be constructed wrt to a regular com-munication between designer and customer in order to re-fine a still abstract specification at the requirements stage continuously into a concrete one at the design stage.5.Conclusions and Further WorkIn this paper an approach has been presented about how human-computer interaction can be specified formally by graph grammars under the consideration of information re-sources.An early and therefore abstract specification can already be used to reason about the system to be designed。