Formal Modelling And Verification Methods For Customized Cyber-physical Production Lines

The trend toward industrial segmentation,product diversification,and manufacturing services in the production sector has been driven by the multi-variety,the variable production model of customization,which has resulted in a sharp decrease in delivery times,more frequent and varied manufacturing tasks,and more complex manufacturing requirements.For specialized cyber-physical production lines,this thesis examines formal modeling and verification techniques.The system model of the cyber-physical components of intelligent production lines has several levels of interaction,and the production model exhibits a long duration.A standard-compliant formal approach to the industrial domain is produced by giving a consistent and accurate description of the domain.In the realm of smart factories,a formal model of dynamic interaction behavior,such as plug-and-play resource sharing amongst production line components,is built.It guarantees that the customized cyber-physical production line’s functional characteristics adhere to the design specifications.This facilitates the multi-granular system level analysis,validation,and deployment of models of customized shop floor components.The main research is summarised in the following four parts.(1)A framework for a dependable formal approach to the factory domain.A concept related to the standardized component description of intelligent production lines by analysing the design requirements and design objectives of formal methods of the factory domain.A formal methodological framework of trusted factory domains based on Model-Data Driven(MDD)is proposed,which integrates a model-driven engineering method with a data-driven concept based on the concept of component partitioning.A domain-specific formal theory and supporting toolchain is constructed based on the above framework.The formal modelling,verification,and performance analysis problems faced when designing systems are verified in real time for the multidimensional dependable modelling requirements and the fusion of heterogeneous resources in the formal approach to cyber-physical production lines in the factory domain.(2)A formal modelling approach for cyber-physical production lines in the factory domain.On the one hand,a normative division of the elements contained in the components of the customized production line of the Cyber-Physical Production Systems(CPPS).A semi-formal modeling approach for production line components based on Extended Formal Process Description(EFPD)is proposed.An intuitive portrayal of the product,process,and resource concepts and the interaction between the three in a production line component.On the other hand,the logic and characteristics of the intelligent production line operation are analysed and a formal modelling language for the customized factory domain is defined.Based on this,a formal metamodel and model on the factory domain is constructed based on the AutomationML data exchange format,which ensures the uniformity of the formal semantics of the production line and the operability of the model.(3)A formal validation mechanism based on dynamic and static resource information about production lines in the factory domain.By describing the attributes related to functional verification,quantitative metrics related to functional verification are proposed.Simulation and verification analysis of a model of an information-physical production line system containing product order information and real-time status information of resources is achieved using a time-coloured Petri net as a Model of Computation(MoC)for the implementation of verification of domain-specific formal models.The model validation results demonstrate that the constructed validation model improves the formal abstraction of the production system and satisfies the various functional properties of the production line layer system at the time of design.(4)A formal mechanism-based approach to Digital Twin(DT)modelling and performance analysis of dynamic systems for cyber-physical production lines.Based on the prototype experimental platform built by the team in the early stage,research on the adaptive operation mechanism of the production line under the action of internal and external disturbances was carried out.Based on the MDD production line modelling method and the operation control tool module,a mapping between formal mechanism-driven physical system simulation and data-driven information system decision-making was established.The final result is model calibration,parameter correction,performance prediction,and analysis of the production line/manufacturing cell.In summary,this thesis presents a theory related to a formal approach to plug-and-play production lines in the context of variable scenarios of external demand or shop floor resources,using customized cyber-physical production lines as the object of study.Improves efficiency and reduces the cost of developing production line systems.Avoiding time or economic losses such as logic omissions and unexpected failures due to customized production.Important theoretical and practical applications can be drawn from this thesis.