# Modeling and Verification of Reconfigurable Printing System Based on Process Algebra

Authors: Rubai Luo; Shasha Gao; Huailin Li; Shisheng Zhou
Journal: Mathematical Problems in Engineering
 (2018)

---

## Abstract

With the print production process as the research object in this paper, the intelligent-context-reconfigurable printing system model is analyzed using process algebra (PA). First, combined with the printing production process, the overall framework of the system model, based on the agent-resource-worker (ARW) component model, is proposed. Abstract and formal verification of the system model are then carried out, and the verification process of the complex calibration process is discussed. Finally, the security and progress attributes of the model are validated by mCRL2. The results show that the system model has good reliability.


---

## Body

## 1. Introduction

As customer demand becomes increasingly varied, demand for product customization and pressure for the rapid introduction of new products are increasing [1]. Traditional manufacturing systems, such as dedicated and flexible systems, cannot provide an adequate response at a reasonable cost and have significant shortcomings in meeting these requirements [2]. Flexible manufacturing systems can convert between different production variants, but they introduce issues of limited flexibility, low productivity, and low return on investment (ROI) [3, 4]. Yoram Koren, a professor who proposed the concept of reconfigurable manufacturing systems for the first time in 1999, thought that reconfigurable manufacturing systems could accurately provide the required functionality [5]. In particular, the modular structure of reconfigurable manufacturing systems enables them to shorten the time to design, build, and redesign a system [6]. Therefore, it is widely thought that reconfigurable manufacturing systems (RMSs) will be very common in the future [7].Reconfigurability is an engineering technology that can help realize rapid, cost-effective responses to market and product changes [8]. Systematic and continuous design and acceleration are the cornerstones of the RMS concept and will appear often throughout its life cycle [6]. Much research has been done on problems related to RMSs [9–16]. The reconfigurability of a printing system is mainly reflected in its ability to change production paths based on product requirements and related environmental changes. Here, “environment” mainly refers to the status of the printing press, material reserves, changes in material interaction and temperature, and humidity in the workshop. This article discusses the design of a contextualized intelligent printing system that can intelligently, dynamically, and quickly configure and organize all kinds of manufacturing systems based on different printed product features.Process algebra (PA) is a formal modeling tool for describing complex systems, and its purpose is to provide a method for studying concurrency and interaction [17]. Process algebra describes the model in algebraic form and defines a complete set of syntax and semantics for the modeled system [18]. The algebraic method based on calculus is now used more in the field of software reusability with fewer applications in RMS [19]. Wei Yaya et al. first attempted to use process algebra to describe a workflow, which provided feasibility verification for manufacturing systems [20]. In addition to using the semantics defined in process algebra and computing rules to verify the viability of a system, the software can be used to validate the reliability of a system [21].The second section of this article introduces operators related to process algebra. The third section discusses the printing system and explains its modeling ideas and workflow. Section4 makes use of process algebra for more complex parts of a system for reasoning and verification, and it is further verified by mCRL2. Section 5 summarizes this article.


## 2. The Introduction of Process Algebra

Process algebra is a high-level algebraic description language that supports the combined description of concurrency, distributed systems and their formal proof of form [17]. It describes the models algebraically, combining subsystems with operators to hide system-unconscious activities of hidden operators, as internal activities and defining a complete set of syntax and semantics for the modeled system. A complete description of process algebra can be found in several references [17, 18, 21–26]. Process Algebra is defined as follows:① Assume a finite, nonempty set A of (atomic) actions, representing indivisible behavior (such as reading or sending a datum). Each atomic action is a constant that can execute itself, after which it terminates successfully:(1)a→a√② “+” is called alternative composition. The closed termt1+t2 represents the process that executes either t1 or t2.③ “·” is called sequential composition. The closed term t1∙t2 represents the process that executes first t1 and then t2.④ “||” is called a merge. This binary operator executes the two process terms in its arguments in parallel. That is, s||t can choose to execute an initial transition of s, an initial transition of t, or communication between s and t.⑤ “|” is called a communication merge. The operation s|t executes as initial transition a communication between initial transitions of the process terms s and t and then behaves as the standard merge operator ||.⑥ “╙” is called a left merge. The left merges╙ ttakes its initial transition from the process terms and then behaves as the merge ||.⑦ “δ” is called deadlock, and it displays no behavior. The communication function γ is extended by allowing the communication of two atomic actions and results in δ, that is, γ:A×A→A∪{δ}. This extension of γ enables us to express that two actions do not communicate by defining γ(a,b)≜δ.⑧ “∂” is the unary encapsulation operator. The ∂Ht can execute all transitions of t whose labels are not in H.⑨ “τ” is a unary abstraction operator, which enables us to abstract away from the internal computation steps of an implementation. For example, τIt expresses that in τIt, all of the labels of transitions of t that are in I are renamed into τ.


## 3. Reconfigurable Printing System Model

Reconfigurable manufacturing systems were first designed to quickly change hardware and software component structures to allow quick adjustment of the production capacity and function of a family of parts due to sudden changes in production requirements [9].The basic process of a printing system is as follows.( 1 ) Prepress stage: process the graphic original to obtain production data that controls the printing and postpress stages.( 2 ) Printing stage: select the appropriate printing process according to production data generated by prepress to transfer the ink, varnish, and other materials to the substrate material surface (such as paper, fabric, or leather) after physical processing and getting the sheet.( 3 ) Postpress stage: apply finishing processes (such as light, hot stamping, die-cutting, and indentation) to the sheet to produce the desired product. After assembly-adaptive processing (such as cutting and folding) the final product is assembled after parts processing (such as stickers, plastic backing, and binding).In the modeling process, the agent-resource-worker (ARW) component is taken as the basic model, and the functions, attributes, and behavior features of the component are abstracted to build agent, resource, and worker models. An agent model describes the type of agent, structure, and realization of the function. A resource model is a collection of various job definition format (JDF) resources. The worker model is an integrated model of the agent and resource models, embodying the final behavior of the ARW component model, as shown in Figure1.Figure 1
ARW component model.Worker models will form a new worker model in different composite ways, with the main composition shown in Figure2, where a is sequential compounding,b is feedback compounding,c is collaborative compounding,d is compounding selection, and e through g are three-component compounds, which can be abstracted as one component and one bicomponent mechanism compound. This can be extended to multiple-component compound mechanisms. In modeling, agents are categorized as executive agents and decision agents. The difference between them is mainly that a decision agent has a context-aware function, which can make decisions according to changes in the environment. An executive-class agent can independently perform its own set of functions. That is, when the agent receives data, it can process it accordingly and then send the processed data to the next agent.Figure 2
Composite approach of worker model.As shown in Figure3, each execution-class agent is named by its function. For example, page making means that the agent is making a page. The workflow simulated by this model is as follows. In the prepress, the first processing of the original is carried out according to the needs of the customer, and the processed file is proofed. It is one step in the printing process. The next step is proofreading. The proofreading is mainly to verify whether the sample is qualified. If the sample is qualified, then the plate is made. Otherwise, the proofing is done again, and the maximum number of samples is nproof. In the printing stage, according to the relevant data obtained in the prepress stage, the decision agent chooses the appropriate printing press and judges whether the materials and workshop environment are suitable for printing and drying. (In the model, No.1 is used to represent the key parts of the intelligent printing system in the context of the different printing presses, which is not described extensively in this article.) In the postpress phase, the decision agent selects the appropriate postprinting procedure according to the preprinted data, and the corresponding agent is executed until the finished product is obtained.Figure 3
Model of reconfigurable printing system.


## 4. Reasoning and Verification

In the reconfigurable printing system model of Figure3, the real line box is mainly aimed at the characteristics of the bounded retransmission communication protocol for the large-data-volume transmission to meet the needs of repeated proofing in the printing process, control the number of samples, and reduce the cost. Due to space limitations, this paper focuses on the verification of the implementation. The rest of the process is executed sequentially, which can be verified according to the algebraic operations in the second chapter.


### 4.1. Model Abstraction

The model is abstracted as shown in Figure4, where A1, K, and A2 are the execution agents, C1 and C2 are counters, and the number of proofs is controlled. The algebraic expression uses the following data parameters and functions: dranges over a finite data set  ∆, and b ranges over 0,1, while n ranges over 0,…,max, wheremax is used to limit the number of transmissions. If max=2, the maximum number of transmissions is three. Finally,ack denotes an acknowledgement message, to denotes count-out, and ⊥ is a data-error message.Figure 4
Abstraction of the model.In this model, A1, K, and A2 are three agents in the system. The algebraic expression of A1 is(2)Xb,n=∑dϵ∆r1d∙Yd,b,nYd,b,n=s2d,b,n∙Zd,b,nn<maxZd,b,n=r5ack∙X1-b,n+r5⊥∙Yd,b,n+1Zd,b,max=r5ack·X1-b,n+r5⊥∙r6to·s7to·STOPThe algebraic expression of K is(3)Vb,n=∑dϵ∆r2d,b,n·Wd,b,nn<maxWd,b,n=s3d,b,n·V1-b,n+s3⊥·Vb,nWd,b,max=s3d,b,n·V1-b,n+s3⊥·s6to·Vb,nThe algebraic expression of A2 is(4)Rb,n=∑dϵ∆r3d,b,n·Td,b,n+r3⊥·UbTd,b,n=s4d,b·s5ack·R1-b,nUb=s5⊥·Rb,n+r7to·Rb,nIn stateXb,n, A1 reads data d from channel 1, after which it proceeds to the Y(d,b,n) state:(5)Xb,n=∑dϵ∆r1d∙Yd,b,nIn stateY(d,b,n), data d is processed by A1, with bits b and n attached to the data. Then the message d,b,n is sent by channel 2:(6)Yd,b,n=s2d,b,n·Zd,b,nIn stateZ(d,b,n), A1 waits for either an acknowledgement or a data-error message (⊥) via channel 5. Suppose A1 receives an acknowledgement from A2. Then, A1 will proceed to state X1-b,n. If A1 receives a data-error message from channel 5 and the number n is less than the maximum, it proceeds to state Yd,b,n+1. Ifn=max, then A1 receives a count-out (to) message from channel 6, and sends a count-out by channel 7. Then, the system issues a warning and implements a manual intervention, which is theSTOP in the algebraic expression:(7)n<maxZd,b,n=r5ack∙X1-b,n+r5⊥∙Yd,b,n+1Zd,b,max=r5ack·X1-b,n+r5⊥∙r6to·s7to·STOPIn stateVb,n, K receives data from channel 2, then it judges the received data and determines whether it is qualified. Then K turns to state W(d,b,n):(8)Vb,n=∑dϵ∆r2d,b,n·Wd,b,nIn stateW(d,b,n), if the data are qualified, K sends a data message via channel 3; otherwise, it sends data-error information through channel 3 if n<max. If n=max, it sends (to) by channel 6 and turns to state Vb,n:(9)n<maxWd,b,n=s3d,b,n·V1-b,n+s3⊥·Vb,nWd,b,max=s3d,b,n·V1-b,n+s3⊥·s6to·Vb,nIn the stateRb,n, A2 waits for the d,b,n. If it receives such a message, then it proceeds to state Td,b,n, in which case it will send the data via channel 4, send an acknowledgement message via channel 5, and turn to state Rb,n. If it receives a data-error message ⊥ from channel 3, it will proceed to state Ub to send this message by channel 5 and directly enter the Rb,n state. It may also receive (to) information from channel 7. And then it will enter the Rb,n state and wait for retransmission:(10)Rb,n=∑dϵ∆r3d,b,n·Td,b,n+r3⊥·UbTd,b,n=s4d,b·s5ack·R1-b,nUb=s5⊥·Rb,n+r7to·Rb,n


### 4.2. Verification Process

Suppose the communication between all agents is successfully implemented in this model. The following equations can be derived fromεACP, commutativity of the merge, and RDP. The proof is as follows.Step 1.
Define the communication:(11)γs2d,b,r2d,b≜c2d,bγs3d,b,r3d,b≜c3d,bγs3⊥,r3⊥≜c3⊥γs5⊥,r5⊥≜c5⊥γs5ack,r5ack≜c5ackγs6to,r6to≜c6toγs7to,r7to≜c7to.Step 2.
Define encapsulation and abstraction operators:(12)H=s2d,b,r2d,b,s3d,b,r3d,b∣d∈∆,b∈0,1∪s3⊥,r3⊥,s5ack,r5ack,s5⊥,r5⊥,s6to,r6to,s7to,,r7to;I=c2d,b,c3d,b∣dϵ∆,b∈0,1∪c3⊥,c5ack,c5⊥,c6to,c7to.The expression for the entire system is(13)τI∂HXb,n∥Vb,n∥Rb,n.
A1 receives the information d and reads the data to carry on proofing, in which b=0,n=0. Proofing is one of the steps in the printing process. And the state of the whole system is(14)∂HX0,0∥V0,0∥R0,0=∑d∈∆r1d·∂HYd,0,0∥V0,0∥R0,0
A1 then sends data d,0,0 by channel 2 to K, and K receives it:(15)∂HYd,0,0∥V0,0∥R0,0=∑d∈∆∂Hs2d,0,0·Zd,0,0∥r2d,0,0·Wd,0,0∥R0,0=c2d,0,0·∂HZd,0,0∥Wd,0,0∥R0,0
K is for proofreading. Proofreading means checking whether the samples are qualified.
① If sample is qualified, then K will send(d,0,0) to A2 and A2 will receive it.(16)∂HZd,0,0Wd,0,0R0,0=∑d∈∆∂HZd,0,0s3d,0·V1,0r3d,0,0·Td,0,0=c3d,0,0·∂HZd,0,0∥V1,0∥Td,0,0
After A2 receives, it will be sent by channel 4, while A1 will send a confirmation message.(17)∂HZd,0,0∥V1,0∥Td,0,0=∂Hr5ack·X1,0∥V1,0∥s5ack·R1,0=c5ack·s4d,0·∂HX1,0∥V1,0∥R1,0
② If the sample is not qualified and the number of times is less thanmax, then K sends (⊥) to A2, and A2 sends feedback information to A1. A1 receives it and reprocesses the original information and (n+1).(18)∂HZd,0,0∥Wd,0,0∥R0,0=c3⊥·c5⊥·∂HYd,0,1∥V0,1∥R0,1n<max
A sends the reprocessed data to K. The data is checked by K.(19)∂HYd,0,1∥V0,1∥R0,1=c2d,0,1·∂HZd,0,1∥V0,1∥R0,1
If the max sample is passed, then(20)∂HZd,0,max∥Wd,0,max∥R0,max=c5ack·s4d,0·∂HX1,0∥V1,0∥R1,0
If the proof fails, the system will stop running(21)∂HZd,0,max∥Wd,0,max∥R0,max=c3⊥·c5⊥·c6to·c7to·STOP
The state transition of∂HX1,0∥V1,0∥R1,0 is the same as that of ∂HX0,0∥V0,0∥R0,0. According to the above verification process, the process chart of the model can be drawn as follows, where 1-5 is the state transition when d=d1,b=0, and 5-1 is the state transition when d=d2,b=0.After application of the abstraction operatorτI, communication actions over the internal channels 2, 3, 5, 6, and 7 are renamed into τ, after which most of these actions can be removed using axiom B1.


### 4.3. Verification with mCRL2

The tools used for process algebra testing mainly include FDR2, the Caesar-Aldebaran toolset (CADP), mCRL2, and LTSA. The mCRL2 has strong interactivity and can intuitively display the migration of each state in the system. Therefore, mCRL2 is used to validate the model in Section4.1. The mCRL2 is a formal specification language with an associated toolset [26] that supports linearization, simulation, state-space exploration, and generation and has tools to optimize and analyze specifications. Moreover, state spaces can be manipulated, visualized, and analyzed. With this language, users can specify the behavior of a distributed system and analyze it using automated techniques [27].The process of verification with mCRL2 is as follows.Step 3.
Write the system process using the mCRL2 language.Step 4.
Convert mCRL2 to linear process specification (LPS). Various operating tools can be used to modify or simplify LPS.Step 5.
Convert LPS to a label transition system (LTS) or state space. This error can then be analyzed using the LTS.Following the above steps, the mcrl2graph tool is used to analyze the generated lts file. The resulting label-migration diagram is shown in Figure6. And the mCRL2 specification of the process is shown in Appendix B. This tool is used to step through the state-transition process and generate a state-transition diagram, as shown below. Throughout the simulation, e0 and e1 represent the additional bits, an max=1, which means that the maximum number of transmissions is two. The state-transition diagram obtained by simulation using mCRL2 is consistent with the system state-migration process of inference in Section 4.2. Among them, the green state point indicates the initial state of the system. At the same time, the repeated transmission part (between state 2 and 3 and state 6 and 7) in Figure 5 is expanded in detail and represented by state point without any color.Figure 5
Process diagram of the model.Figure 6
State-transition diagram of the system.


## 4.1. Model Abstraction

The model is abstracted as shown in Figure4, where A1, K, and A2 are the execution agents, C1 and C2 are counters, and the number of proofs is controlled. The algebraic expression uses the following data parameters and functions: dranges over a finite data set  ∆, and b ranges over 0,1, while n ranges over 0,…,max, wheremax is used to limit the number of transmissions. If max=2, the maximum number of transmissions is three. Finally,ack denotes an acknowledgement message, to denotes count-out, and ⊥ is a data-error message.Figure 4
Abstraction of the model.In this model, A1, K, and A2 are three agents in the system. The algebraic expression of A1 is(2)Xb,n=∑dϵ∆r1d∙Yd,b,nYd,b,n=s2d,b,n∙Zd,b,nn<maxZd,b,n=r5ack∙X1-b,n+r5⊥∙Yd,b,n+1Zd,b,max=r5ack·X1-b,n+r5⊥∙r6to·s7to·STOPThe algebraic expression of K is(3)Vb,n=∑dϵ∆r2d,b,n·Wd,b,nn<maxWd,b,n=s3d,b,n·V1-b,n+s3⊥·Vb,nWd,b,max=s3d,b,n·V1-b,n+s3⊥·s6to·Vb,nThe algebraic expression of A2 is(4)Rb,n=∑dϵ∆r3d,b,n·Td,b,n+r3⊥·UbTd,b,n=s4d,b·s5ack·R1-b,nUb=s5⊥·Rb,n+r7to·Rb,nIn stateXb,n, A1 reads data d from channel 1, after which it proceeds to the Y(d,b,n) state:(5)Xb,n=∑dϵ∆r1d∙Yd,b,nIn stateY(d,b,n), data d is processed by A1, with bits b and n attached to the data. Then the message d,b,n is sent by channel 2:(6)Yd,b,n=s2d,b,n·Zd,b,nIn stateZ(d,b,n), A1 waits for either an acknowledgement or a data-error message (⊥) via channel 5. Suppose A1 receives an acknowledgement from A2. Then, A1 will proceed to state X1-b,n. If A1 receives a data-error message from channel 5 and the number n is less than the maximum, it proceeds to state Yd,b,n+1. Ifn=max, then A1 receives a count-out (to) message from channel 6, and sends a count-out by channel 7. Then, the system issues a warning and implements a manual intervention, which is theSTOP in the algebraic expression:(7)n<maxZd,b,n=r5ack∙X1-b,n+r5⊥∙Yd,b,n+1Zd,b,max=r5ack·X1-b,n+r5⊥∙r6to·s7to·STOPIn stateVb,n, K receives data from channel 2, then it judges the received data and determines whether it is qualified. Then K turns to state W(d,b,n):(8)Vb,n=∑dϵ∆r2d,b,n·Wd,b,nIn stateW(d,b,n), if the data are qualified, K sends a data message via channel 3; otherwise, it sends data-error information through channel 3 if n<max. If n=max, it sends (to) by channel 6 and turns to state Vb,n:(9)n<maxWd,b,n=s3d,b,n·V1-b,n+s3⊥·Vb,nWd,b,max=s3d,b,n·V1-b,n+s3⊥·s6to·Vb,nIn the stateRb,n, A2 waits for the d,b,n. If it receives such a message, then it proceeds to state Td,b,n, in which case it will send the data via channel 4, send an acknowledgement message via channel 5, and turn to state Rb,n. If it receives a data-error message ⊥ from channel 3, it will proceed to state Ub to send this message by channel 5 and directly enter the Rb,n state. It may also receive (to) information from channel 7. And then it will enter the Rb,n state and wait for retransmission:(10)Rb,n=∑dϵ∆r3d,b,n·Td,b,n+r3⊥·UbTd,b,n=s4d,b·s5ack·R1-b,nUb=s5⊥·Rb,n+r7to·Rb,n


## 4.2. Verification Process

Suppose the communication between all agents is successfully implemented in this model. The following equations can be derived fromεACP, commutativity of the merge, and RDP. The proof is as follows.Step 1.
Define the communication:(11)γs2d,b,r2d,b≜c2d,bγs3d,b,r3d,b≜c3d,bγs3⊥,r3⊥≜c3⊥γs5⊥,r5⊥≜c5⊥γs5ack,r5ack≜c5ackγs6to,r6to≜c6toγs7to,r7to≜c7to.Step 2.
Define encapsulation and abstraction operators:(12)H=s2d,b,r2d,b,s3d,b,r3d,b∣d∈∆,b∈0,1∪s3⊥,r3⊥,s5ack,r5ack,s5⊥,r5⊥,s6to,r6to,s7to,,r7to;I=c2d,b,c3d,b∣dϵ∆,b∈0,1∪c3⊥,c5ack,c5⊥,c6to,c7to.The expression for the entire system is(13)τI∂HXb,n∥Vb,n∥Rb,n.
A1 receives the information d and reads the data to carry on proofing, in which b=0,n=0. Proofing is one of the steps in the printing process. And the state of the whole system is(14)∂HX0,0∥V0,0∥R0,0=∑d∈∆r1d·∂HYd,0,0∥V0,0∥R0,0
A1 then sends data d,0,0 by channel 2 to K, and K receives it:(15)∂HYd,0,0∥V0,0∥R0,0=∑d∈∆∂Hs2d,0,0·Zd,0,0∥r2d,0,0·Wd,0,0∥R0,0=c2d,0,0·∂HZd,0,0∥Wd,0,0∥R0,0
K is for proofreading. Proofreading means checking whether the samples are qualified.
① If sample is qualified, then K will send(d,0,0) to A2 and A2 will receive it.(16)∂HZd,0,0Wd,0,0R0,0=∑d∈∆∂HZd,0,0s3d,0·V1,0r3d,0,0·Td,0,0=c3d,0,0·∂HZd,0,0∥V1,0∥Td,0,0
After A2 receives, it will be sent by channel 4, while A1 will send a confirmation message.(17)∂HZd,0,0∥V1,0∥Td,0,0=∂Hr5ack·X1,0∥V1,0∥s5ack·R1,0=c5ack·s4d,0·∂HX1,0∥V1,0∥R1,0
② If the sample is not qualified and the number of times is less thanmax, then K sends (⊥) to A2, and A2 sends feedback information to A1. A1 receives it and reprocesses the original information and (n+1).(18)∂HZd,0,0∥Wd,0,0∥R0,0=c3⊥·c5⊥·∂HYd,0,1∥V0,1∥R0,1n<max
A sends the reprocessed data to K. The data is checked by K.(19)∂HYd,0,1∥V0,1∥R0,1=c2d,0,1·∂HZd,0,1∥V0,1∥R0,1
If the max sample is passed, then(20)∂HZd,0,max∥Wd,0,max∥R0,max=c5ack·s4d,0·∂HX1,0∥V1,0∥R1,0
If the proof fails, the system will stop running(21)∂HZd,0,max∥Wd,0,max∥R0,max=c3⊥·c5⊥·c6to·c7to·STOP
The state transition of∂HX1,0∥V1,0∥R1,0 is the same as that of ∂HX0,0∥V0,0∥R0,0. According to the above verification process, the process chart of the model can be drawn as follows, where 1-5 is the state transition when d=d1,b=0, and 5-1 is the state transition when d=d2,b=0.After application of the abstraction operatorτI, communication actions over the internal channels 2, 3, 5, 6, and 7 are renamed into τ, after which most of these actions can be removed using axiom B1.


## 4.3. Verification with mCRL2

The tools used for process algebra testing mainly include FDR2, the Caesar-Aldebaran toolset (CADP), mCRL2, and LTSA. The mCRL2 has strong interactivity and can intuitively display the migration of each state in the system. Therefore, mCRL2 is used to validate the model in Section4.1. The mCRL2 is a formal specification language with an associated toolset [26] that supports linearization, simulation, state-space exploration, and generation and has tools to optimize and analyze specifications. Moreover, state spaces can be manipulated, visualized, and analyzed. With this language, users can specify the behavior of a distributed system and analyze it using automated techniques [27].The process of verification with mCRL2 is as follows.Step 3.
Write the system process using the mCRL2 language.Step 4.
Convert mCRL2 to linear process specification (LPS). Various operating tools can be used to modify or simplify LPS.Step 5.
Convert LPS to a label transition system (LTS) or state space. This error can then be analyzed using the LTS.Following the above steps, the mcrl2graph tool is used to analyze the generated lts file. The resulting label-migration diagram is shown in Figure6. And the mCRL2 specification of the process is shown in Appendix B. This tool is used to step through the state-transition process and generate a state-transition diagram, as shown below. Throughout the simulation, e0 and e1 represent the additional bits, an max=1, which means that the maximum number of transmissions is two. The state-transition diagram obtained by simulation using mCRL2 is consistent with the system state-migration process of inference in Section 4.2. Among them, the green state point indicates the initial state of the system. At the same time, the repeated transmission part (between state 2 and 3 and state 6 and 7) in Figure 5 is expanded in detail and represented by state point without any color.Figure 5
Process diagram of the model.Figure 6
State-transition diagram of the system.


## 5. Conclusions

Based on process algebra, this paper constructs a reconfigurable printing system model using an ARW component model. By abstracting and verifying the system model using process algebra, the inference results show that the system can fulfill the expected functions. Using mCRL2’s security and schedule attributes on the system model, its execution is in line with the actual printing process and has good reliability.



---

*Source: 9189836-2018-10-04.xml*