Analysis for the composition of information flow security properties on Petri net

The analysis and verification of complex systems are often encountered by researchers. The best way of solving this problem is using some simple or small systems to compose the complex system and the characters will be preserved. However, because the definition of information flow security properties are based on different semantic model, it is difficult to carry out a systematic discussion of composition. We analysis three security properties which have been defined on the unified model of Petri net and give the conditions in which the property will not be changed. And we give the proof of these conclusions. Because there are too many compositions for Petri net, the task will be huge if researchers discuss each of them. Therefore, we put these compositions under a unified framework which can improve efficiency. In this framework, the compositions of Petri net are classified into two types and the conditions which can keep the security properties of original net are given.