| The application of embedded systems plays a very important role in modern life.From a small smart water meter at home to the construction of the entire smart city,embedded systems are indispensable.Embedded systems have specific functionalities,and it requires a lot of effort to perform error checking after the development is completed.Therefore,modeling and analyzing embedded systems in the early stages of system design can effectively reduce system errors and improve system design efficiency.Modern embedded systems often have a large scale,and the division of internal functions is also relatively complicated.For example,the construction of a smart city includes multiple system modules such as smart transportation,smart medical care,and smart home.Each system module consists of several smaller functional modules,when the traditional PRES+(Petri net based Representation for Embedded Systems)is used for system modeling,high modeling complexity arises and it is difficult to clearly divide the functions.OOPN(Object-Oriented Petri Net)combines the object-oriented thinking in the Petri net structure,which is suitable for modeling the system with clear function division.Therefore,combining the structural characteristics of PRES+ and OOPN,integrating object-oriented thinking into PRES+ structure,and the embedded system model OOPRES+(Object-Oriented Petri net based Representation for Embedded Systems)is obtained.The OOPRES+ not only has a strong description ability for embedded systems,but also can clearly describe different functional modules of the system with the help of object-oriented structure.The internal implementation of each functional module is hidden,and a fixed interface is left for information exchange.When using the OOPRES+ to model a modular complex embedded system,the number of reachable identifiers in the net model will "explode" due to the complexity of the system itself,making the analysis of the model properties much more difficult.Therefore,it is necessary to take some measures to alleviate this problem.In order to improve the efficiency of model analysis and alleviate the problem of "state space explosion",this thesis proposes the following synthesis methods: the synthesis operation method of shared single transition gateway,the synthesis operation method of shared transition gateway set,the synthesis operation method of shared single object subnet,the synthesis operation method of shared object subnet set.With the synthesis operation,two embedded system models can be composited into a single embedded system model.In addition,this thesis has carried out a maintenance analysis of the liveness,boundedness,reachability,timing,and functionality of the synthetic system,which improves the analysis efficiency of the original model.In order to verify the effectiveness of the synthesis method,the modeling and analysis of the road traffic vehicle information acquisition system based on the intelligent transportation system and the indoor environment control system in the smart home system based on the smart home system in the smart city were carried out.The results also proved the rationality of the proposed OOPRES+ structure and the feasibility of the synthesis operation rules. |