document: A framework for XML data streams history checking and monitoring 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 .
doc_bio_tags: O O O B O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O