Modeling Web Applications by the Multiple Levels of Integrity Policy

We propose a formal method to validate the reliability of a web
  application, by modeling interactions among its constituent objects.
  Modeling exploits the recent "Multiple Levels of Integrity"
  mechanism which allows objects with dynamically changing reliability
  to cooperate within the application. The novelty of the method is
  the ability to describe systems where objects can modify their own
  integrity level, and react to such changes in other objects.  The
  model is formalized with a process algebra, properties are expressed
  using the ACTL temporal logic, and can be verified by means of a
  model checker.  Any instance of the above model inherits both the
  established properties and the proof techniques. To substantiate our
  proposal we consider several case-studies of web applications,
  showing how to express specific useful properties, and their
  validation schemata. Examples range from on-line travel agencies,
  inverted Turing test to detect malicious web-bots, to content
  cross-validation in peer to peer systems.