Istituto di Scienza e Tecnologie dell'Informazione     
Amato G., Coppola M., Gnesi S., Scozzari F., Semini L. Modeling web applications by the multiple levels of integrity policy. In: 1st International Workshop on Automated Specification and (Valencia, Spain, Mar.14--15 2005). Proceedings, pp. 161 - 176. M. Alpuente, S. Escobar, M. Falaschi (eds.). Elsevier Science, 2005.
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.
Subject web
formal method
D.2.4 Software/Program Verification
F.3.1 Specifying and Verifying and Reasoning about Programs

Icona documento 1) Download Document PDF

Icona documento Open access Icona documento Restricted Icona documento Private


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional