| Navigation of a web application is the possible sequences of pages accessible to a user. Navigation is more complex when adaptive navigation is involved, that is, when the navigation depends on user mode (e.g. logged-on users or VIP users) or previously visited pages. Thus it is difficult to precisely specify the desired navigation behavior and ensure that the specified is the intended behavior. To implement navigation a developer must decide the request routes, which is the sequence of components that handle each web page request. Because these components use event-based communication and the navigation-related code is spread across a number of components, it is difficult to understand the request routes and hard to ensure the implemented navigation behavior conforms to the navigation design.; To solve these problems, I first developed FARNav (Formal Approach for Rich Navigation) to formally model an application's navigation behavior. FARNav uses Statecharts to explicitly represent adaptive navigation and can automatically verify navigation rules. No other existing navigation model explicitly represents adaptive navigation and provides automatic verification for navigation behavior.; Next I created a formal model (the Request Routing Model) to describe how requests are routed through server components. Analysis operations are defined for the request routing model to automate tasks such as tracing request routes. No other model explicitly represents request routing and support automatic tracing for the request routes.; These two models are related in that both describe navigation behavior: one in terms of how different modes affect the navigation links, and the other in terms of how the implementation accomplishes the navigation.; I define mappings from the FARNav model to the request routing model and vice versa. Then I show that the mappings preserve navigation behavior and they are bijective. I provide a Model Helper tool that implements the mapping. Thus a developer can specify and check the navigation behavior, then automatically generate and check a corresponding request routing model with full tool support. After making changes to the request routing model, the developer can automatically extract the FARNav model from the request routing model to check whether the navigation behavior is still preserved. |
