A framework for XML Data Streams History Checking and Monitoring

• Alessandro Campi, Politecnico di Milano, Italy
• Paola Spoletini, Politecnico di Milano, Italy

Full text:

Track: Posters

The need of formal verification is a problem that involves all the fields in which sensible data are managed. In this context the verification of data streams became a fundamental task. The purpose of this paper is to present a framework, based on the model checker SPIN, for the verification of data streams. The proposed method uses a linear temporal logic, called TRIO, to describe data constraints and properties. Constraints are automatically translated into Promela, the input language of the model checker SPIN in order to verify them.