L. Grigore and U. Buy (USA)
Petri nets, formal methods, supervisory control.
Web applications are often based on the client-server model which relies on concurrent execution of asynchronous pro cesses. Enforcing correctness of concurrent software is no toriously difficult. In general, automatic verification checks if a given system has a certain property, while supervisory control enforces the same property by restricting system behavior. Supervisor control problems are often computa tionally more tractable to solve than verification problems. Most verification problems are NP-hard, while some super visory control problems can sometimes be solved in poly nomial time with the appropriate representation. Here we present two algorithms, one for enforcing mutual exclusion and the other for deadlock prevention, for web applications written in Java. We combine these two methods in order to guarantee that a web application or web service comply with given safety properties including freedom from dead lock and system specific mutual exclusion properties.
Important Links:
Go Back
