On the application to OSI-TP of a structured analysis and modelingmethodology based on Petri net models

摘要

An application of the Petri-nets for the formal modeling andnanalysis of a distributed transaction processing tree, based on OSI-TPn(transaction processing) and OSI-CCR (commitment, concurrency andnrecovery) mechanisms for the two phase commit procedure, is made. Innorder to cope with the complexity of the system (a tree structure and anmultiple association architecture), the authors develop a methodology ofnstructured modeling, based on the abstraction concept. Abstraction isnalso used for verification purposes. Abstractions based on threenequivalence relations (trace, failure, observational equivalence) arenconsidered. Their interest for the modelization and the verification ofnthe provided TP service are shown. Comparisons are also made