Designing reliable Web-based information systems is not trivial. Authors need to allow as much flexibility in navigating through the system as possible on the one hand, and to ensure the satisfaction of properties and constraints in the system on the other. The problem is aggravated with facilities like CGI scripts and Java applets which incorporate dynamic behaviour into the information structure. These issues motivate the need for designing such systems through rigorous modelling and analysis. We observe similarity between Web-based information systems and distributed systems and relate the two by adopting the Calculus of Communicating Systems (CCS), a process calculus for modelling distributed systems, to capture such features of a Web-based information system as its navigational st...[ Read more ]

Designing reliable Web-based information systems is not trivial. Authors need to allow as much flexibility in navigating through the system as possible on the one hand, and to ensure the satisfaction of properties and constraints in the system on the other. The problem is aggravated with facilities like CGI scripts and Java applets which incorporate dynamic behaviour into the information structure. These issues motivate the need for designing such systems through rigorous modelling and analysis. We observe similarity between Web-based information systems and distributed systems and relate the two by adopting the Calculus of Communicating Systems (CCS), a process calculus for modelling distributed systems, to capture such features of a Web-based information system as its navigational structure, semantics, dynamic behaviour and browsing semantics. Properties like the ordering constraint, reachability and coverage constraint are then expressed as modal μ-calculus formulae so that verification can be carried out in an automatic fashion using some model analyser. We also identify features of Web-based information systems unique to ordinary distributed systems and propose corresponding changes in property-checking algorithms such that model checking can be more meaningful and comprehensive. Next, we explore several ways to apply our approach to domains like information retrieval and examine how useful it is. Before we conclude, a case study is investigated to demonstrate the practicality of our approach.