The International Journal of Advanced Manufacturing Technology (2018) 98:1505–1521 https://doi.org/10.1007/s00170-018-2089-4
ORIGINAL ARTICLE
Formal modeling and verification of a part manufacturing systems using FSZ-automaton with CLS criteria Shazada Muhammad Umair Khan 1
&
He Wenlong 2
Received: 6 November 2017 / Accepted: 26 April 2018 / Published online: 20 June 2018 # Springer-Verlag London Ltd., part of Springer Nature 2018
Abstract Failures in manufacturing systems reliant on human operators must address the issues of coverage, liveness, and starvation (CLS) to prevent accidental interactions among the component of the system or accidental human-automation interaction (HAI). Manufacturing systems would benefit from techniques that lay the ground work for investigating the possible rectifications for problems that might cause down time. The formal verification is the dominant technique utilized, along with mathematical proof that shows that an accordingly scaled model of a manufacturing system contains the desired properties of the large real-world manufacturing systems. This paper describes a method of FSZ-automaton, which combines finite-state machine model with Zschemas for establishing concurrency and a distributed structure within manufacturing systems. FSZ-automaton was used to complete the formal verification of the part manufacturing system. This formal verification is also used to validate FSZ-automaton, its usability properties, and to distinguish the mode confusion. Moreover, the advances in formal verification continue to address these issues, such that the traditional analysis procedure is validated and can potentially avoid this constraint. Keywords Z specification . Schema . Manufacturing . Automata . Formal model
1 Introduction Currently, in an automotive industry, there are multiple requirements on many different specialized purposes that apply in design and development of a manufacturing cell. For the development and design, an extensive amount of money is always required [1] and there is ever-increasing competition in the market [2], which necessitates the need to mitigate costly mistakes in the manufacturing design process before proceeding to construction and development of manufacturing cell. The second most important requirement is that the machinery and advanced manufacturing system must accomplish an operation in the least amount of time possible. BBC
* Shazada Muhammad Umair Khan
[email protected] He Wenlong
[email protected] 1
Department of Industrial and Information Engineering, Hanyang University, Ansan, Gyeeonggi-do, South Korea
2
Department of Mechanical Engineering, Hanyang University, Ansan, Gyeeonggi-do, South Korea
Business News reported that Toyota recalled 190,000 vehicles due to the faulty manufacturing of suction plates which could have caused a fuel leak and had a high probability of unsafe ignition. More efficient manufacturing systems are required to produce product variety to compete within this manufacturing environment. By modeling of the part manufacturing system correctly, success within this industry can be greatly improved. Simulation and modeling [3] are the two techniques that are invaluable in the design and analysis of part manufacturing systems. The importance of predicting the reliability and quality [4] of part manufacturing systems within a modeling framework is useful in order to satisfy the formal specification of the manufacturing system [5]. Furthermore, the framework of formal modeling, and the validation and verification of the same, will resolve many issues in part manufacturing systems and it will ensure formal specification requirements [6] are consistently met. Simulation and formal modeling provide a framework to aid [7] formal validation and formal verification. There is considerable existing research, where the formalization of the methods has been documented [8]. However, issues remain a part of manufacturing cell representation using formal specification their verification and validation. Furthermore, the existing methodologies for formal specification and its
1506
verification had not been applied to the manufacturing cell test case. Currently, there is no published research to represent the manufacturing cell with these modeling techniques. Within the literature, the manufacturing system was analyzed graphically with tree diagrams, theoretically and through graphical specification. The main issues to overcome in modeling that manufacturing part system are its complexity, the specificity of each different manufacturing cell, and representing the true system reasonably. All the issues can be resolved by applying the methodologies of formal modeling. The goal is to formalize the use of modeling for part manufacturing cell specification requirements, through the development of unambiguous and robust modeling that has been well refined and verified. The CLS acronym stands for coverage, liveness, and starvation. Coverage is based on a computational concept that measures whether the structure is achievable. Liveness is defined as having a system that will execute the user and machine tasks as per the system requirements. Starvation is when there is no need to perform an extra task by the user to avoid the system blocking. This research is different from other publications in that it is a combination of the two most well-known formal method approaches: finite-state machine with Z-schemas using CLS criteria. These two methods have been applied in different fields of research. The latest research on the finite-state machine is a graphical representation showing the system states and their transitions that illustrate the manufacturing structure and its dynamic behavior. With all these benefits, it is still incomplete with respect to the power of formal modeling, desire for refinement, and data abstraction. To eliminate these limitations, the researcher developed other variants of finite-state machine [9] but it was still lacking further enhancement to make it reliable and efficient within part manufacturing systems. Abstract and algebraic state machines are two examples of these variants [10, 11]. Z-schemas (Z) take the form of a formal notation [12] that represents the system specification consecutively. It is based on set builder notation and higher-order predicate logic to aid the formal interpretation. It is still lacking though, in terms of completing the adequate definition of the simultaneous and shared systems. It is also not accurate on working semantics. The combination of the different formal models, however, is a new domain for enhancing, understand and analyzing a complex system. Very few scientists have taken the approach of combining the Z with CSP and CCS models [13–15]. The goal of this research is to extend the finite-state machine by utilizing the effectiveness of data definition and function using Z-notation. The Z is also developed with accurate working semantics and with simultaneous manufacturing system using a finite-state machine. The most excellent advantages that we get after combining of finite-state machine to Z are as follows:
Int J Adv Manuf Technol (2018) 98:1505–1521
a. A combined formal model to capture different aspects of a manufacturing system (data types, framework, performance, and control flow) b. A cooperative formal model to simulate contrasting types of a manufacturing systems (subsequent, appropriated, and simultaneous) c. A well-documented report of interdependent development of formal specification and reasoning techniques d. An updated method and concept from the combination Formal verification is the technique for doing an analysis of the complex system. It is a subset category of formal methods. Formal methods are used for specification development, complex system modeling, and their verifications [16]. The formal specification describes the complex system properties in correct and explicit notations. The complex systems are modeled based on mathematical languages that aid in the theoretical formalism denoted finite-state automata. Finally, the mathematical techniques used for the verification process of a complex system must be evaluated to determine whether the specification is satisfied or not. As a part of verification techniques, there is a verification of a part manufacturing system using analysis of FSZ-automaton. The remainder of this paper contains the literature review, the definition of FSZ-automaton, a description of the FSZautomaton development approach, and the system verification using FSZ-automaton analysis. An illustrative example of a part manufacturing system is presented using FSZ-automaton and verification of the same, followed by the conclusions and the direction of future research.
2 Literature review FSZ-automaton is an advanced formal modeling technique meaning it is concerned with high-level finite-state machines [17] within which high-level transition function has been used. Findings within this paper are compared to previous work with respect to common technology and the novel aspects of this approach. Formal modeling [18] of a complex system provides the descriptive, analytic, abstract [19], concise, complete, unambiguous [20], maintainable, and rigorous tools and technique that consist of basic set notation [21]. It facilitates the adequate construction of formal specification application. In manufacturing systems, formal modeling is widely used. The supervisory control [22] theory can be achieved in the context of finite-state machines [23]. Further advancement has been made in the software development [23] by implementing the formal specification. Currently, the formal modeling representation of manufacturing systems in terms of abstraction have sizable gaps in descriptive, analytic, abstract, concise, complete, unambiguous, maintainable, and rigorous tools and technique. The manufacturing system is
Int J Adv Manuf Technol (2018) 98:1505–1521
1507
still equipped with a few abstraction parameters as shown in Table 1 and considers the characteristics of formal reasoning [25]. Additionally, formal modeling is divided into two categories [36]; one is the machine-based technique and another one is the language-based technique. A machine-based technique consists of finite-state automata and specification description language [37, 38]. The language-based technique is used in devices [30] having the synchronous languages such as CSL, Luster, Signal, and Esterel that describe the system behavior. Most of the research has been conducted using theoretical and conceptual models, but few scientists represent the modeling of manufacturing systems using syntax [24], and few researchers have highlighted the importance of the meaningful representation of manufacturing systems using semantics-based analysis [39]. The manufacturing system must be a complete, concise, and expressive conceptual model, including syntax and semantics-based representation, explicitly using formal modeling. However, the theory of automata places attention on the formal modeling of a manufacturing cell that utilizes finite-state machines which are also referred to as abstract computing machines. In contrast to the finite-state machine, the Z specification [40] is a method to structure the mathematics with objects and properties that are collected in the form of schemas. This schema is used to define the state of the system and the type of change within Table 1
the system. Within this paper, the system properties and their refinement were defined using schema. There is however a limitation in attempting to express the complex system performance with control, functionality, data abstraction, and refining to explicitly define the operational semantics [18, 32–34]. The Z specification has the capability of set-based notation and building its own specification but if there is an action involving a procedure, then Z is not a suitable method. The advantage with Z specification is that it is well-accepted with its defined operations. Examples of this include schema representation [27], proving [41], and model checking [33, 42]. To complete the requirement analysis of manufacturing systems [35], we must consider its characteristics in terms of performance, integration, structure, control, and program optimization [26, 28]. Based on this, Z was applied to formulate the system requirements of manufacturing systems in terms of program optimization. There were only a few scientists that performed research [43] related area on the FSZ-automaton [44]. To adequately specify manufacturing systems, both aspects (behavioral as well as data-oriented) must be considered. Therefore, Z was used to specify the data-oriented aspects of the manufacturing system. Combining the finite-state machine and Z languages generates the understandable, simpler, and improved complex scheme-based representations for analysis. After this
Comparison with previous literature
S# Authors System types
System aspect
Modeling Abstraction
Distributed FR Integration DAS MP Structure Control DA Functionality DR DB EOS
1 2
[24] [25]
Se, Sy Sy
A, Ma, Con Com, Ma, Con
√ √
√
L L
√ √
3 4 5 6 7 8 9
[19] [26] [27] [28] [29] [30] [31]
Se, Sy Se, Sy Se Sy Se Sy Se
A, Ma, Con A, Ma, Con Com, Ma, Con Com, Ma, Con Com, Ma, Con A, Ma, Con A, Com, Con
√
√ √ √ √ √ √ √
M M L M M M L
√ √ √
[20] [32] [33] [34] [18] [15] [9] 17 [35] Our
Se Se Sy Sy Se Sy Sy Se Se, Sy
U, M, Com A, U, Ma, Com Con, Com, U A, Con, Com U, Ma, Com A, U, Ma, Con A, U, Con, Ma A, Com, Con A, Con, Com, U, Ma √
10 11 12 13 14 15 16
√ √
√ √ √ √ √ √ √ √ √
√
√
√
√
√ √ √
√ √ √
√ √
M M L L L L
√
L M H
√ √ √
√ √ √ √ √ √ √
√ √ √ √ √
√
√ √
√
√ √
√ √
√
√ √ √
√ √
√ √
√ √
√ √
√
√ √ √
√ √
√
√ √
√ √
√ √
Se semantics, Sy syntax, L low, M medium, H high, √ available, A abstract, Con concise, Com complete, U unambiguous, Ma maintainable, FR formal reasoning, DAS development and analysis of specification, MP modeling power, DA data abstraction, DR data refining, EOS explicit operational semantics, DB dynamic behavior
1508
Int J Adv Manuf Technol (2018) 98:1505–1521
combination, there are compensations including system aspects and system type requirements using formal representation. To do the comparison of our work with previous work has shown in Table 1. The combination of methods within this paper is represented as an FSZ-automaton and the solution method is presented in Table 2. The solution method is applied for formal modeling of manufacturing systems that have issues as described in previous literature has shown in Table 1. The verification of the method is also provided using FSZ-automaton. The FSZ-automaton is a branch of a high-level finite-state machine that is like a high-level finite-state machine. The FSZ-automaton is concerned with further work on development of Z with simultaneous execution of formal model and mechanisms. In the formal model, attention toward coherent modeling is necessary. In Z-schemas, the entire formal specification consists of modeling, abstraction, system aspect, and system type properties that define an organogram of automaton construction. Single comprehensive condition representation completely states that single transaction representation will be to individual state change duration [29]. Representation of state change duration is transmitted to receive the operative meaningful proof for the syntax using applications for the variables of incoming and outgoing. The novel contribution of the present work within this paper is to manage the simultaneous and distributed nature of FSZ-automaton. It is by describing the single condition-based scheme individually that the state object including single condition-based schemes then become applicable process
Table 2
schemes. The FSZ-automaton achieved useful semantics using hidden variables. Z is used in the scheme to express the data structure and its abstraction. This approach is also support for method development and investigations of technique. In high-level finite-state machine that consists of a basic finitestate machine model such as state transition. The algebraic finite-state machines consist of algebraic specification using formal modeling. FSZ-automaton use Z-notation based on rigorous and unambiguous specification. These models are equal in the power of expressiveness. In an algebraic finite-state machine, the implementation of the algebraic specification is still lower level than Z specification in FSZ-automaton. It is very important that the algebraic specification is more difficult to understand as compared to Z-schemas. The important features of FSZ-automaton are as follows: a. The elemental formalism of FSZ-automaton has been widely applied and accommodates specification using Znotation. Z allows extensive procedures to process the information, definition including concept. Individually, Z schemes for FSZ-automaton use easy mathematical statements, as well as reasonable and purposeful descriptions for the different advanced finite-state machines. b. The FSZ-automaton control flows at a low level and the structures having known restrictions could recover using common comprehensive information constructions given using Z scheme. Moreover, the use is well understood for
Solution method System
Solution method
S# 1 2
System Modeling aspect Language
3 4 5 6 7 8 System type 9 10 11 12 13 14
Distributed Formal reasoning (FR) Integration Development and analysis of specification (DAS) Modeling power (MP) Structure Control Data abstraction (DA) Functionality Data refining (DR) Dynamic behavior (DB) Explicit operational semantics (EOS)
Include [syntax + semantics] with a formal set of rules, propositional logic, meaningful information for expression and rules analyze for expression, properties prove, predicate Abstract [logical lay out, conceptual model, schema with a collection of variables, operations, predicate, concise [free types, set with explicit structuring information], Complete [Every information covered, all possible variables, schema conjunction]. Maintainable [reflecting the charges] Predicate with equality, one-point rule, types, set comprehension, free types, schemas Propositional logic, predicate logic, relations and functions FSZ-automaton Syntax, semantics, refinement, theorem proving High [by verifications, proofs, FSA + Z, schemas, data types, relation on schema operators Schemas, promotions, free and constraints promotions Z specification, proofs, refinement, automation Schemas and preconditions, initializing theorem properties Relation and functions, functions on relations, function on sequence overriding Specification lead towards suitable implementation, refine one partial relation to other The concept of backward and forward simulations Free types and primitive recursions
Int J Adv Manuf Technol (2018) 98:1505–1521
common information structures giving higher suppleness for describing the possible consistently. Simultaneous manufacturing is a good example. This merging generates formal specification issues such as states that are not inconsistent. To protect against these issues, the validity of FSZ-automaton using the formal specification process must be maintained c. It is applicable for processing of data based on the fact there are several existing outputs to determine Z. The other finite-state machine models are executable, so the reachability analysis which is suitable to FSZ-automaton. Due to having the Z specification, the invariant analysis cannot be applied directly to FSZ-automaton. Past research has improved the simultaneous model execution using Z to aid in the representation of formal modeling and the properties analysis of a complex system associated with the parallel processing of these two models. By using the illustrative example, the method also proves its applicability to a complex problem. This novel method is concurrent and much more descriptive than any other model. The working semantics are used for complex system modeling and their simulation. The major novel achievement from this model is the simultaneous execution using schemas. These schemas used by Z-notation describe the system properties following the temporal logic approach. To model the working semantics, Z was applied. By comparing to the FSZ-automaton, it is easier to understand because of its highly graphical representation and explicit execution model. To analyze this model for formal verification [31] that is a subset of formal methods, the formal specification is used to define the system properties with the aid of formal modeling. This formal modeling will satisfy the formal specification that covers the domain of formal verification. In this paper, formal verification using the analysis of FSZ-automaton helps to understand the formal model which satisfies the system requirement specification.
3 FSZ-automaton In this section, the combined approach of Z-eve and finitestate automaton (FSA) is described through the importance of comprehensible formalism termed FSZ-Automaton. The generic application of FSA is to express inclusive architecture, system behavior, and control schemas used in Z-eve to describe the data structure and abstraction. The value of data is constrained and describing these variables and functional processing is termed schema. In the form of tuple, the high-level FSA is expressed as ⟨Ma, Mz, M(a × z)〉 [45], in which Ma is FSA, Mz is an underlying specification in Z-eve, and M(a × z) is used for the set to link the assistant components of FSA including an individual description for Mz. Likewise, Spec is used for algebraic state machine requirements [45, 46]. In
1509
FSA-Z, Spec is contained in a set of schemas using Z-notation. This combined approach seizes those physical objects and events of the uncontrolled manufacturing system, which are relevant for the development of modeling the manufacturing system. The model is separated into the semantics of the static model and semantics of the dynamic model. A formalism of FSA-Z representation was applied in an illustrative case for clearer understanding of the formalization.
3.1 Semantics of the static model The static semantics model comprises FSA, schemas, and proximity of FSA and schemas in Z-eve. Our FSZautomaton is a tuple of ⟨Ma, Mz, M(a×z)⟩ where Ma = finite-state automaton, Mz = schemas in Z-eve, and M(a×z) = proximity of FSA and schemas in Z-eve. The element of tuple comprises a description of data types for physical objects. These objects are parts, machines, and performance of an operation at a certain state. The executions of these operations are based on certain manufacturing operations which may lead toward the desired state. Now, each tuple element will be discussed in the following subsections.
3.2 Finite-state machine 〈Ma〉 Attention was drawn toward the operator behavior during the manufacturing system utilizing the finite-state automaton. It is used to represent the consistent transition of the discrete system. The finite-state machine is a mathematical model that consists of a finite number of states and transitions that specify manufacturing system behavior based on state changes using predefined rules. The finite-state automaton can be defined as a six-tuple. Ma ¼
Σa ; Qa ; ðqa Þ0 ; δa ; F a ; Δp
Where Σa is the input alphabet (a finite non-empty set of symbols); Qa is a finite, non-empty set of states; (qa)0 is an initial state such that (qa)0 ϵ Qa; δa is Σa × Qa → Qa the state transition function; and Fa is the set of final states such that Fa ⊆ Qa. Δp A description of all the possible transitions. Formally, Δp is a function Δp: Qa × {ΣaU{∈}} → ℙ(Qa) is the power set of Qa. To illustrate the finite-state machine, the part manufacturing process must be considered. In our case, there are three processes required to finish the part. The first one is the cutting process, the second one is the boring process, and the final one required to finish the part is the reaming operation. The state of the operation is represented as Qa = {q0 = cutting, q1 = boring, q2 = reaming}, while the set of actions are ∑a = {∑al = cutting operation length = 3 mm, ∑a2 = boring operation dimension = 15 mm, ∑a3 = reaming operation dimension =
1510
5 mm}. The transitions will happen after the boring manufacturing operation is applied to the part to the new state q2 from the previous state q1. The gathering of all relevant information to describe the manufacturing operation state is termed as schema. The schema comprises two elements. The first element consists of declaration, where the variables are defined. The second element consists of predicate, where the variable is given initial values. If we need to represent the finite-state machine using the schema, then the schema of finite-state machine is as follows:
In the declaration, the variables are declared for the finite-state machine, while the predicate initiates the variables. The manufacturing operations states are the Qa = {q0 = cutting, q1 = boring, q2 = reaming}. The set of actions are ∑a = {∑al = cutting operation, ∑a2 = boring operation, ∑a3 = reaming operation}. The state transitions will occur after the execution of the initial state.
3.3 FZ specification using schemas 〈Mz〉 The gathering of relevant information to describe the manufacturing operation state is defined as schema. In this paper’s scenario, schema 〈Mz〉 is a three-tuple having a collection of the schema. 〈Mz〉 = SchQ,SchΣz,Sch(q) f,Sch(q)0 is a collection of schemas in Z-eve [47] to describe the element of state and restrictions including the preliminary state of 〈Ma〉. Sch is defined as a schema using Z specification. The name(sch), declaration(sch), and predicate(sch) symbolize the definition, declaration format (captured as map between the sets), and the definition of predicate using in schema. The schemas representation through Z must satisfy these given conditions: ∀sch1 ; sch2 : SchQ ðsch1 ≠sch2 ⇒dec ðsch1 Þ∩dec ðsch2 Þ ¼ φÞ; ∀sch1 ; sch2 : SchðqÞ 0 ðsch1 ≠sch2 ⇒dec ðsch1 Þ∩dec ðsch2 Þ ¼ φÞ; SchQ ¼ SchðqÞ 0
a. At starting, the above two predicates explain that schemas are pairwise disjointed. b. The last condition specifies that both schemas are in equal number.
Int J Adv Manuf Technol (2018) 98:1505–1521
3.4 Proximity of FSA and Z specification using schemas M(axz) The finite-state machine Ma with Z specification Mz becomes M(axz) in the form of tuple which can be described as follows: D E M ða zÞ ¼ Qða zÞ ; Σða zÞ ; δða zÞ ; qða zÞ0 ; qða zÞ f where Qða zÞ : Qa → SchQ is based on the definition of Ma. At every state, qa ϵ Qa, Qða zÞ always maps qa to a unique schema sch ϵ SchQ such that qa = name (sch). The type of qa is defined by the predicate in the schema. In the schema representation, the name of the schema is a set of states to describe the system. The states with the predicate of initial and the final state are defined. In manufacturing processes, when it starts is termed as the initial state and the completion state is called the final state. In terms of manufacturing process, the cutting operation is the initial state and the reaming operation is the final state.
Σ(a×z) : Σa → SchQ is one-to-one mapping based on the definition of Ma. For each transition Σa qa ∈Σa Qa : ΣðazÞ map to Σa x qa to a Schema sch ∈SchΣz · Σa × qa = name (sch). The property of the schema is defined as the functional processing of Σa x qa. In the schema representation, the schema defines the name of the set of actions in terms of the alphabet. For the manufacturing process, the set of actions will be cutting, boring, and reaming operations. Moreover, the following constraint will be satisfied.
For any qa ϵ Qa, Σa × qa ϵ Σa × Qa: a: If ðqa ; Σa Þ∈Σa Qa then dec QðazÞ ðqa Þ ∩ dec ΣðazÞ ðΣa qa Þ ≠φ;
b: If ðΣa ; qa Þ∈δa then dec QðazÞ ðqa Þ ∩ dec ΣðazÞ ðΣa x qa Þ ≠φ;
δða zÞ : δa → ϖHvar is the reachable state of Ma. The Hvar is the hidden variable based on quantification in SchΣz. Hvar(Σa) shows in the form of set for hidden variables in Σða zÞ (Σa)
Int J Adv Manuf Technol (2018) 98:1505–1521
used for any transition Σa. The sort (v) shows the kind for inconstant v. The sort (v) shows the variable including set for sorted set (v) thus the following constraints must be satisfied.
1511
abnormal states and transitions will not satisfy these criteria, as shown within the counterexample.
3.6 No blocking state (liveness) a. δ(a × z) `(qa, Σa) ⊆ v(Σa) and δ(a × z) `(Σa,qa) ⊆ v(Σa), Where b. δ(a × z) `(i,j) = δ(a × z) (i,j) iff (i,j) ∈ δa or otherwise φ. c. For any i ∈ δ(a × z) `(qa, Σa) (or δ(a × z) `(Σa,qa)), sort(i) ∈ sort (dec(Q(a × z) (qa)); d. Pred(Σða zÞ (Σa)) ⟹ dec(δða zÞ (qa)`) = dec (δða zÞ qa) δða zÞ `(qa, Σa) ∪ δða zÞ `(Σa, qa); In the schema representation, the name of the schema is defined in terms of the transition. The state of transition is defined with sets of actions and the execution of the transition is done using the state of systems to generate the new state. In short, the execution of the action will allow the transition from the current state to the new state. The process of transition is defined in terms of its declaration and predicate. Similarly, the state moves to reaming operation after executing the boring operation and that will be the final state of the manufacturing operation.
The user or system that may block the system will not satisfy the liveness property. To satisfy it, there must be no deadlock state during the user and machine task execution. To verify it, the counterexample will not generate the desired state. The system is reachable if and only if there is no counterexample and the user must have satisfied the final state of the system.
3.7 All task must finished (starvation) The executed user task must eventually finish. If it happens, then it will satisfy these criteria. The blocking state will generate if the task will not finish and the user needs extra resources to finish the task. The halt task may be generated in the counterexample to understand better the task blockage. The CLS properties are free from any abnormal state and must perform successful task execution to reach the desired state.
4 CLS-based properties
qða zÞ0: Qa → Schq0 is a sort respecting dec (Qða zÞ (qa)) = dec (qða zÞ 0 (qa)) initial state of Ma where Schq0 is a schema defining the initial state qða zÞ0 of qa state. By using the characterization, it is helpful to determine the given properties. The proposed formal modeling of a manufacturing system gives analytic, abstract concise, complete, unambiguous, maintainable, and rigorous tools and technique that consist of basic set notation. The manufacturing system model is a complete, concise, and expressive conceptual model including syntax and semantics-based representation explicitly using formal modeling. This paper’s model overcomes this limitation, in trying to express the complex system performance. To complete the required analysis of the manufacturing systems, the specific characteristics of performance, integration, structure, control, and program optimization were considered.
3.5 Reachable computational structure (coverage) Within the coverage criteria, the user task must be reachable. All the states in FSZ and all the transitions must be fulfilled to accept the coverage criteria. The criteria are fulfilled when all states are reachable, and all transitions are executed. To verify all the states and transitions, it will move as per the standard fashion to satisfy the CLS properties. The generation of
There is only one major schema representing the data category of the individual state using Qða zÞ . There is another Qða zÞ respecting schema defining the current position of the individual state in the FSZ-automaton. FSM has a distributed nature through secured data allocation so there are no incidental inconsistent system states that may occur. a. One schema describes the performance of individual transition using Σða zÞ . It consists of pre-and post-conditions with an unmarked and marked variable. Pre-condition describes the state in ready mode, while post-condition describes that the state as executed. b. The tagging of the variables are treated as a hidden variable inside the state that is ready for transition execution to change the state in the corresponding schema using δ(a × z). The sort type variable emerges when matching unseen inconstancies with the schema. It is necessity and reliable in including near sort state. c. If the states are connected by the transition after consistent schemas are connected variable states for were used. In addition, there is a change in the schema which is consistent with the transition defined by Ma.
5 Semantics of dynamic model The FSZ-automaton is mapping qða zÞ : Qa → dec (SchQ). This state is belonging to the schema of SchQ.
1512
a. Based on the locating state qða zÞ , the transition is Σa × qa ϵ Σa × Qa. The state is ready for transition at qða zÞ if it will follow the following predicate. Ready current transition qða zÞ (Σa×qa) is true pre- Σ ða zÞ (Σa×qa). b. If the state is ready for transition execution at qða zÞ , then the locating state emerged out (q(a × z))` if the following predicate q ( a × z ) (Σ a ×q a ) is true: post-Σ ða zÞ (Σa×qa). (qða zÞ `(qa) = qða zÞ (qa)- δða zÞ (qa, (Σa×qa)): δða zÞ ((Σa×qa), qa) for Qa ∈ qa. c. In order to locate qða zÞ , the set qða zÞ of reachable locating from qða zÞ is the least set of locating such that (qða zÞ )` ∈ qða zÞ and (qða zÞ )`((Σa×qa))(qða zÞ )`` then (qða zÞ )`` ∈(qða zÞ ) for (Σa×qa) ∈ (Σa×Qa). d. The formation of current state is being executed then the previous state is reachable from q (a × z) ϵ Q for Σa x qða zÞ → Σa × Qa. e. The formation of a sequence of FSZ-automaton is (Σa×q(a × z))0. (Σa×q(a × z))1 when FSZ-automaton is finite.
Int J Adv Manuf Technol (2018) 98:1505–1521
Sch(q)0 = {Init Lock Jig, Init Weld, Init Unlock Jig}.
The Z-automaton behavior is valid for the executed sequence, starting from the initial state.
6 An example Discussed below is a simple example of FSZ-automaton specification for a weld shop station. The weld shop system design has been shown in Fig. 1. The automaton structure Ma = ⟨Σa, Qa, (q0)a, δa, Fa⟩ is described here: The schemas are ⟨Mz⟩ = ⟨SchQ, SchΣz, Schq(q)f,Sch(q)0. SchQ = {Lock Jig, Weld, Unlock Jig}.
The M ða zÞ is defined as follows: Qða zÞ Σ ða zÞ δða zÞ
{q (a × z)1 → Lock Jig, q(a × z)2 → Weld, q(a × z)3 → Un Lock Jig} {Σ(a×z)1 = Spot Welding, Σ(a×z)2 = Hanging Spot Gun} {(q(a × z)1,Σ(axz)1) → lj, (q(a × z)2,Σ(a×z)2) → w, (q(a × z)3, Σ (a×z)3) → uj, (Σ (a×z)1,q (a × z)1 ,) → lj`, (Σ(a×z)2,q(a × z)2,) → w`, (Σ(a×z)3,q(a × z)3,) → uj`}
n o qðazÞ0 ¼ qðazÞ1 →Lockjig
ð1Þ
n o qðazÞ f ¼ qðazÞ3 →Unlock Jig
ð2Þ
While in FSZ-automaton, schema state and variable state are described graphically. It is part of the state in Z-automaton. SchΣz = {Spot Welding, Hanging Spot Gun}.
7 Significant features of FSZ-automaton The important features of FSZ-automaton are highlighted within this section through the relationships between Z-eve and finite-state machines. This may also help in the development of the FSZ-automaton specification.
Int J Adv Manuf Technol (2018) 98:1505–1521
1513
lj
W`
W
uj`
lj`
W
W`
uj
Lock
Spot Welding
Jig
Hanging Spot Gun Weld
Unlock Jig
Fig. 1 Z-automaton specification of the part manufacturing system, Q = {Lock Jig, Weld, Unlock Jig}, Σa = {Spot Welding, Hanging Spot Gun}
7.1 Main characteristics
8.1 State transitions
The observations are as follows:
The finite-state machine that describes the behavior of a complex system, including the effect, circumstances, and consequences of transition, is expressed by schema linked with FSZ-automaton transition. In Z, the transition is expressed by schema stating the components of the complex system. Based on conditions, the action of schema is a change in the state transition-based system. In this example, it is before the machining operator loads the part and after the machining operator unloads the part. Both activities can change the state of the part manufacturing system. Using the above definition, the following combines the automata with Z-schemas that exists in FSZ-automaton.
a. The complex system structure is modeled by finite-state automaton explicitly, which makes it more comprehensible rather than indirect using schemas. b. In Z-notation, it is very complex and not possible to define the state execution to uphold it in FSZ-automaton. In FSZ-automaton, the state transitions are simpler and only in schemas in Z-notation such that the transitions consist of numbers and a variety of schemas.
8 System states The state of the finite-state machine is defined by the location of the state. Each state is based on structured data. These states describe the status of a feature within a complex system. The states are Lock jig, Weld, and Unlock Jig as shown in Fig. 1. In formal specification by using Z-notation, the state of the system is defined by the schema and its list shows the component of the complex system. Every schema will have the state variable that expresses the current condition of a complex system component. From Fig. 1, the schemas of a part manufacturing system state are as follows: SchQ = {Lock Jig, Weld, Unlock Jig}.
a. When the schema includes no change Ξsys at its part declaration, then there are two arrows in opposite directions. The first one is away and the second one is the inward direction. b. When the operation in schema includes the state change Δsys is in the declaration, then one of the following will be true. c. Omitting the state transition. d. Incrimination of transition to the state. e. Update the opposite direction using a different tag connecting the transition to the state.
8.2 Variables in FSZ-automaton The variables occur within the state are in the form of a tag and the constrained link with transitions. These variables are very near to transition and show the equivalent variable identification appearing in the form of the tag. The variables are placed in the form of a tag at inward and outward direction within the state or near to transition activation. In Z-notation, there are input, quantity, and a state variable. This variable is used in name, declaration, and predicate part. In this context, the variable in finite-state machine is linked with input and output variables in schemas. Moreover, based on the literature,
1514
Int J Adv Manuf Technol (2018) 98:1505–1521
confined tags are used to quantify variables, which maintain the consistency between the FSM and schemas, and provides the simple structure of FSZ-automaton.
8.3 Formation of FSZ-automaton The technique to build FSZ-automaton specification was used. Analytics for developing the FSZ-automaton and performing modifications to the existing FSZ-automaton were utilized. Analytics maintained the specific features and constructs to complete FSZ-automaton, while the alteration maintained the validity of FSZ-automaton.
To preserve the validity of alteration ensures the right semantics and syntax. The following alteration rule shows FSM structure and schemas accommodate each other in FSZautomaton for the validation of an integral system specification. The alteration guidelines manage system operation before and after alteration. It provides the acceptable instruction for mandatory system investigation with altered FSZ-automaton. This system analysis is much simpler than investigating the FSZ-automaton from the beginning. & & & &
9 Analytics The representation of a complex system describes the interaction with the environment as well as the system components and its control flows. After all, the finite-state machine is a graphical representation of system components and their control flow, as shown in Fig. 2. Each event is described by finite-state machine to represent its state and transition. The resulting finite-state machine is the behavioral model of the complex system. The finite-state machine contributes a comprehensive foundational view of a complex system. Using this model, the inconsistent and incomplete requirements of the system are recognized. The FSZ-automaton defines the model behavior. The schema using Z-notation provides the semantics of static model behavior. The states schema must be constructed for every state with a specific type. In the schema, the declaration describes the comparable state. For an event representation, the operation of the schema for every transition must be described. The constraints of transition are in the predicate. The above guidelines are the major developments in constructing the Z-automaton. Using these guidelines, initial Z-automaton specifications were generated and are outright and executable. Finally, the system behavior can be simulated. If there is a minor change in Z-automaton, then validity must be checked. For validity, alteration is studied in the following section.
Fig. 2 The control flow concept of system component representation through finite-state machine using schema
10 Alteration considered with CLS
& & & & & &
& & & & &
The increment of new predicate while deleting the predicate is a reverse process. The increment of sch1 to SchQ and sch2 to Σ ða zÞ . Increment of (qa, Σa×qa) to Q(a × z) and (qa, sch2) to qða zÞ . The increment of a new transition while deleting a transition will follow the opposite process. The increment at sch to SchΣz. The increment of (Σa×qa,sch) to Σ(a×z). Addition of new arrow (qa, Σa×qa) or (Σa×qa, qa) to δa and the deletion of arrow is a reverse process. Adjusting Σ(a×z) (Σa×qa) by adding the schema name Q(a × z)(qa) in declaration part. Adjusting δ(a × z) so the variable in the new label δ(a × z) (qa, Σa×qa) or δ(a × z) (Σa×qa, qa) are as hidden variable Σ(axz) (Σa×qa). Suppose that q1 and q2 are the two states having the same preset and posttest now merge them while dividing a state q into new state q1 and q2 is the counter process of that given below. The increment of new state qa to Qa. Increment of new arrow (qa, Σa×qa) to Σa×qa → Qa if (q1, Σa×qa) ϵ Σa×qa → Qa and the increment of ((qa, Σa×qa), δ(a × z) (q1, Σa x qa) ∈ δ(a × z) (q2, Σa×qa)) to δ(a × z) . The increment of ((Σa x qa, qa), δ(a × z) (Σa x qa,q1) ∈ qa (Σa x qa,q2)) to qa. The increment of new schema sch2 to SchQ achieved by employing conjunction operation to Q(a × z) (q1) and Q(a × z) (q2) and taking an increment of (qa, sch1) to Q(a × z). Incrimination of new schema sch2 to Schq0 achieved by employing schema conjunction operation to schema q(a × z)0 (q1) and q(a × z)0 (q2) and incrementing (qa, sch2) to q(a × z)0.
1) Complex system
2) FSM representation of
3) Define static
representation
a complex system
semantics
4) Schema design
4) Design the operation schema design for individual transition
Int J Adv Manuf Technol (2018) 98:1505–1521
& &
& &
& & &
Omitting q1 and q2 from Qa the linked arrow is from Σa×qa → Qa and the linked schema is from SchQ. Combining the two-different transitions having the same preset and post set: (Σa×q)1 and (Σa×q)2 having two transitions, after applying the merging operation while the dividing is the reverse process. The increment of new transition (Σa×qa) to (Σa×Qa). Increment of new arrow (qa, Σa×qa) to Σa×qa → Qa if (qa, (Σa×qa)1) ∈ Σa×qa → Qa and incrementing in ((qa, Σa x qa), δ(a × z) (qa, (Σa×qa)1)) to δ(a × z). The handling of dissimilar tag, it is necessary to define the new tag having new tag operator. Now divide the schema in two different schemas and each arrow map to schema. Increment of ((Σa×qa), qa), δa × z ((Σa×qa)1, qa) to δ(a × z). The increment of new schema sch to SchΣz achieved by formation of schema disjunction operation to Σ(axz) (Σa×qa)1 to Σ(axz) (Σa×qa)2. Omitting (Σa x qa)1 and (Σa x qa)2 from (Σa x Qa) the linked arrow from Σa x qa → Qa and the linked schema sch to SchΣz.
For merging the two-sequential transition, suppose that (Σa×qa)1 and (Σa×qa)2 are the two sequential transition linked with state q through arrow ((Σa×qa)1, qa) and (qa (Σa×qa)) including (Σa×qa)1 and (Σa×qa)2 are the only transition linked with q. While dividing the transition into two joined transitions using a new state q is the counter procedure of that given below. The merging operations are as follows: & &
& & & &
The increment of new transition (Σa×qa) to (Σa×Qa). Increment a new schema to sch to SchΣz achieved by employing schema composition operation to Σ(axz) (Σa×qa)1 and Σ(axz) (Σa×qa)2 and omitting the q in sch. Increment a new arrow (qa (Σa×qa)) to Σa×qa → Qa if (qa, (Σa×qa)1) ∈ Σa×qa → Qa and incrementing in ((Σa×qa), qa), δ(a × z) ((Σa×qa)2, qa) to δ(a × z). Incrementing ((Σa×qa), qa), δ(a × z) ((Σa x qa)2, q) δ(a × z). Omitting transition q from Qa its linked schema Q(a × z)(q) from SchQ and q(a × z)0 (qa) from Schq0. Omitting transition (Σa×q)1 and (Σa×qa)2 from (Σa×Qa) their linked schemas from SchΣz and their linked arrow Σa×qa → Qa.
1515
10.2 Analyzing the behavior property of FSZ-automaton Behavior properties can be easily analyzed using the reachability technique. It is applicable to FSZ-automaton since it is executable, and every new current state can be evaluated by a consistent schema. It is the most influential interactive examination performance.
10.3 Analyzing the invariant properties of FSZ-automaton The properties that never change for the subclass behavior of system characteristics are referred to as invariant properties. The invariants of the system should be satisfied at every state and all accessible states in FSZ-automaton, since the schemas based on Z-notation are first-order logic and set builder notation are typed in set theory. It is recommended that for subsequent techniques, the invariants of system properties for FSZautomaton be investigated.
10.4 Analyzing the invariant properties of FSZ-automaton Suppose that [(q(a × z)0)ψ] expresses all the valid current states extracted from all sequence executions of an FSZautomaton. The υ is the valid state execution, | υ| is the length of output sequence, and υ(i) is the ith state in υ. Δpinv is the invariant property if its hold: ∀ υ : υ∈ [[(q ( a × z ) 0 ) ψ ]⦁ (∀ i: 0 ≤ i ≤ | υ |⦁ (υ(i)| = Δp i n v ⦁ (υ(i)| = Δpinv)))] where (υ(i)| = Δpinv describes the indicating υ(i) satisfies Δpinv. Hence the safety property holds each state (indicating) of all valid location sequence. In simplified form of the set of all reachable locations only; h i ∀qðazÞ : qðazÞ ∈ qðazÞ0 qðazÞ j ¼ Δpinv
10.5 Proving invariant properties The basic invariance rules: X1: q(a × z)0 ⇒ Δpinv X2: Σ(a × z) (Σa × qa): Δpinv ⇒ Δpinv` for each (Σa × qa) ∈ (Σa × Q) / q(a × z)| = Δpinv for every q(a × z)∈ q(a × z)0
10.1 Verification using the analysis of FSZ-automaton Finite-state automaton has two properties for analyzing. One of them is behavior and the other is structural properties. Behavior property is closely related to the program verification, which will be discussed in the following section.
As a defined rule, evidence X1 needs the original location q(a × z)0 to infer property Δpinv and evidence X2 needs full transition preserves Δpinv. Σa (Σa × qa) and is the schema that is associated with the transition. Δpinv` is achieved from Δpinv through altering names for variables. X1 including X2 saw a Δp achieved that is effective and fulfilled underneath an
1516
Int J Adv Manuf Technol (2018) 98:1505–1521
accessible pattern through q(a × z)0. The research delivers these guidelines: Step1: Must prove the initial location that validates the system property. Step 2: Suppose that the property of system grips after k measures including the state q (a × z). Final step must be to verify that invariant if the system satisfies the k + 1 measures through many directional accessible states through q (a × z).
machining will be performed when checking the quality of parts and their availability. This FSZ-automaton is not complete, and requires more refinement using schemas. 2) Based on the requirements of part manufacturing systems, two events will occur, which are loading and unloading, and both require the part validation. 3) The FSZ-automaton structure developed three state schemas for part in, machining, and part out. The schemas for part in, machining, and part out are as below: The schemas ar {SchQ, SchΣz, Sch(q)f, Sch(q)0}. SchQ = {Part in, Machining operation, Part out}.
11 Illustration This section illustrates a potential example scenario for the methods developed. Consider that at the weld side, the operations are not executed as the system demanded. The welding part was wrongly fitted on the weld jigs. Initially, a team member believed the problem was linked with the parts. After a plant investigation by the group leader, the problem was identified with the jigs. The dimensions of the jigs parts did not meet the standard criteria. The downtime was noted on average daily basis to be 20 min at the jig shop and 35 min at weld line. The process of part manufacturing is performed using CNC machines at jig shop. After finishing the manufacturing operations, the part is fixed into the welding jig to ready for performing the weld operations. In this example, the operator loaded a part into the CNC machine. After loading it into the machine, the machining operation must be performed. Only then can it move into the next station as shown in Fig. 3. In this part manufacturing system, the first operation is part loading and the second one is part unloading. Moreover, the following constraint must be satisfied, which is that machining operations can be performed on all parts to be machined.
The part description containing the details of name, associated vendor, and type (either use for left/right and the partial function of their part number). In machining, the operator loads the part in. After loading the part, machining will be performed. The machining operation will consist of drilling, reaming, and boring.
Finally, part out describes that either the part exists or not in the rack. If it is existing, then it means machining operations have been done on it successfully; otherwise, the part is not in condition for machining.
12 Development of FSZ-automaton specification 1) The requirements of this are part in, machining, and part out. Analytics were applied to the part manufacturing system. There are three states and two transitions. The first one is loading and the last one is unloading as shown in Fig. 3. The Fig. 3 A structure of an FSZautomaton for part manufacturing system
pi pi`
4) In this stage, we can define the initial condition of schemas using the Z-notation.
mc`
mc
po`
mc
mc`
po
Loading Part in
Unloading Machining
Part out
Int J Adv Manuf Technol (2018) 98:1505–1521
1517
There are nth parts in system initially. Early dimensions of machining are well-defined through using the schemas. There are n machining operations that need to be performed on the parts, then all parts are unique. 6) In this step, the FSZ-automaton structure and the tag variables are achieved as a part of hidden variable.
At initially all the parts are ready to perform the machining operation.
5) The loading of the part into the machine always requires the machining operation validity and part availability before performing the machining operation. The input requires the part information and machining operation information. In the predicate part, there are hidden variables defined. In the second and third line, there is a check that the part validity and the remaining parts show the availability of machining operation on the part, which will affect the status of a part. SchΣz = {Loading, Unloading}.
The unloading operation of the part is a counter process of loading the part into the machine.
The alteration of second to third increment of innovative transition of loading error is applied. Also, linked hidden variables are showing that there is a possible loading error. The FSZautomaton was shown in Fig. 4. The transition of loading was renamed to loading ok. Connection of schema with loading error uses the given data structure intended for messages: MESSAGE::=“wrong part” | “cannot perform machining” | “part is not available.” The downtime was reduced to be on average daily to be 10 min at the jig shop and 20 min at the weld line side.
1518
In the schema, the variable in terms of output msg! to report the loading error is received. For every line that explains the quantification of the predicate part using schemas, it described the specific loading error. Now the alteration 5 was applied for loading error and loading ok by getting the update transition of loading. After investigating the FSZ-automaton as similar to Fig. 3, the schemas for loading were explained with he help of given disjunction: Loading≙Loading ok ∨ Loading error. With expertise about the part manufacturing system, and after revision of above process schemas the alteration 4 was applied to achieve the FSZ-automaton in Fig. 4. Lastly, alteration 6 for splitting the transition of loading into two transitions was completed for part validation and check loading, shown in Fig. 5. The subsequent schemas are as given as follows:
The schemas for a new transition like for part validation and check loading are as follows:
Int J Adv Manuf Technol (2018) 98:1505–1521
[48, 49] SAL pseudo code. This translation was updated to safeguard the manufacturing system to not reach the error or deadlock state. Although it is acceptable to perform operations again, if and only if the system reached the finished state. For example, finishing the part manufacturing operations. The manufacturing machine operations automation and machine– human interface were created straight in the model checker [48] manufacturing system specification.
14 Verification of part manufacturing system using FSZ-automaton analysis The part manufacturing system constraint is a requirement of the manufacturing system as follows: ∀qðazÞ ∈qðazÞ0 ð∀hpn; v; pnoi↦pi∈qðazÞ ðPartsÞ ðpi∈
It is not complex to do the verification of alteration 6 to validate the transition of part validity and check loading as shown in Fig. 5. The schema linked with loading is same as described by loading ok ∨ loading error. By applying this technique, the part manufacturing is per industry standard, and parts that are then fitted into the jigs and the jigs that are arriving into the weld shop are to specification.
∪
mc→part name∈qðazÞ ðPart statusÞ
mc∪
∪
mc∈qðazÞ ðPart statusÞ
mcÞÞ
where q(a × z) (parts) = part and q(a × z)(part status) = mc` ∪ part in. It is rewritten again to the above specification to omit the explicit application of q(a × z). ∀mc ∈ ran part⦁ (mc ∈ part in ∈ ∪ dom mc) (*) The above characteristic is the system invariant and now is proving the (*) in Z-automaton in Fig. 5. Step1: For initial Init machining ran part = part in ∪ dom mc Step2:
13 Design investigation The form of the model was changed into SAL with the help of a translator. This translator was accompanying the 180 lines of
Suppose that (*) holds K changes in state of q(a × z): q(a × z) (parts) = part and q(a × z)(part status) = mc ∪ part in likewise ∀mc ∈ ran part (mc ∈ part in∪ dom mc).
Int J Adv Manuf Technol (2018) 98:1505–1521 Fig. 4 A refined FSZ-automaton for part manufacturing system
1519
pi pi`
mc`
mc
po`
mc
mc`
po
Loading ok
Unloading Machining
Part in
Loading error
Part out
mc mc`
Fig. 5 A refined FSZ-automaton for part manufacturing system
pi pi`
mc`
mc
po`
mc
mc`
po
Unloading Machining
Part in
Part out
Check loading Part validation ps
ps`
Part status
ps` ps
Step3: To show that (*) after k + 1 changing in a state q(a × z)` such that q(a × z)[(Σa × q(a × z)) q(a × z)`] for a transition Σa × q(a × z) with generation of q(a × z)`(parts) = part`, q(a × z)`(Part status) = mc`∪ part in. ∀mc ∈ ran part`⦁ (mc ∈ part in` ∪ dom mc`). To do the examination of transition for part validation, there is no effect in the state of part validation hence (*) still holds. The transition at part inspection for first and third disjunction since mc` = mc then there is a part in` = part in and machining` = machining. The second disjunction mc ∈ part in ∧ part in` = part in | {mc} ∧ mc` = (mc, first(ps)) ∧ machining` = machining ∪ {mc`} ∧part` = part. part in` ∪ dom machining` = part in ∪ dom machiningpart1 = part. By replacing the induction assumption: ∀mc ∈ ran part`⦁ (mc ∈ part in`∪ dom machining`).
Since all possible transition from a given current state q(a × z) has been measured with preserve all property (*), (*) including the proved through sequential logical induction technique.
15 Results through formal verification To perform the formal verification, a personal computer having Mint 18.2 with i5 processor, 2 G bytes RAM was utilized. The result obtained from the model checker through the SAL required 20 s to verify the model properties and resulting in 1456 determined number of reachable states at one verification. This result was higher than expected. Every transition was as described by the model in the Fig. 3 associated with all states is reachable. In addition, no counterexample has been produced to visualize it further.
1520
16 Conclusions The modeling of a complex manufacturing system based on user understanding is not descriptive, analytic, abstract, concise, complete, unambiguous, maintainable, and rigorous as a manufacturing system and product quality demand. This is because of user and system interactions that were not expected by analysts and designers. Further, the scientists had not anticipated the importance system features and types, due to several user-machine interactions when the process of manufacturing is ongoing. To meet this need, a formal framework was developed for the analysis of human–computer interaction systems, with modeling based on FSZ-automaton using CLS properties. Compared with other models, this novel approach describes the formal models of user and supervisor activities with machine behavior by adopting the modeling techniques of FSZ-Automaton with full control and mode preserving under the consideration of CLS properties. It is also proposed that the formal verification is the dominant technique with mathematical proof that an accordingly scaled model of a manufacturing system that may contain the desirable CLS properties. In this paper, we developed FSZ-automaton combined with finite-state machine and Z-schemas for establishing concurrency and distributed structure of a manufacturing system. Formal verification of part manufacturing systems was completed by using the analysis of FSZ-automaton. Moreover, this formal verification is also used for the validity of FSZautomaton. In addition, the advances in formal verification continue to address outstanding issues and the traditional analysis procedure can potentially avoid this constraint. The technique was implemented in a case study of weld shop activities. This study helped to reduce the down time during two operations, saving 10 and 20 min, respectively. For future work, a possible extension would be to add information about the environment and a cognitive model of the system and user. Such information constitutes a user and supervisor statebased interface. The supervisor and user models for such systems can be advanced in the sense that their transitions should be well defined. Defining the generation of such an interface is a possible extension of this work. Finally, with this method, the advances in formal verification continue to address known issues, improving the traditional analysis procedure.
Int J Adv Manuf Technol (2018) 98:1505–1521
References 1.
2.
3.
4.
5.
6.
7.
8.
9.
10.
11. 12. 13. 14.
15.
16. 17. 18.
19.
Acknowledgments We thank Hanyang University for providing the support for this research and conducting visits and experiment of car manufacturing industries by the support of Hanyang University.
20.
Publisher’s Note Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
21.
Sanders NR, Graman GA (2009) Quantifying costs of forecast errors: a case study of the warehouse environment. Omega 37:116– 125 Anwar S, Sun S (2012) Trade liberalisation, market competition and wage inequality in China's manufacturing sector. Econ Model 29:1268–1277 Cicirelli F, Furfaro A, Nigro L (2011) Modelling and simulation of complex manufacturing systems using statechart-based actors. Simul Model Pract Theory 19:685–703 Sun J-w, Xi L-f, Du S-c, Ju B (2008) Reliability modeling and analysis of serial-parallel hybrid multi-operational manufacturing system considering dimensional quality, tool degradation and system configuration. Int J Prod Econ 114:149–164 Zaytoon J (1996) Specification and design of logic controllers for automated manufacturing systems. Robot Comput Integr Manuf 12:353–366 Evrot D, Pétin J-F, Méry D (2006) Formal specification of safe manufacturing machines using the B method: application to a mechanical press, in 12th IFAC Symposium on Information Control Problems in Manufacturing, INCOM'06, Saint-Etienne, France, CDROM Edgar S-M, David M-V (2014) State of the art in the research of formal verification. Ingeniería, Investigación y Tecnología 15:615– 623 Khan SMU, He W (2018) Formal analysis and design of supervisor and user interface allowing for non-deterministic choices using weak bi-simulation. Applied Sciences, 8(2):221 Bolton ML, Bass EJ, Siminiceanu RI (2013) Using formal verification to evaluate human-automation interaction: a review. IEEE Trans Syst Man Cybern Syst 43:488–503 Börger E, Stärk RF (2003) Abstract state machines: a method for high-level system design and analysis; with 19 Tables. Springer Science & Business Media Conway JH (2012) Regular algebra and finite machines: courier corporation Smith G (2000) The object-Z specification language, vol 101. Citeseer Benjamin M (1990) A message passing system. An example of combining CSP and Z, in Z User Workshop, pp. 221–228 Taguchi K, Araki K (1997) The state-based CCS semantics for concurrent Z specification, in Formal Engineering Methods., 1997. Proceedings., First IEEE International Conference on, pp. 283–292 Imran M, Young B (2015) The application of common logic based formal ontologies to assembly knowledge sharing. J Intell Manuf 26:139–158 Wing JM (1990) A specifier's introduction to formal methods. Computer 23:8–22 Caines PE, Wei Y-J (1995) The hierarchical lattices of a finite machine. Syst Control Lett 25:257–263 Li M, Wei J, Zheng X, and Bolton ML (2017) A Formal Machine– Learning Approach to Generating Human–Machine Interfaces From Task Models, IEEE Transactions on Human-Machine Systems Bolton ML, Bass EJ, Siminiceanu RI (2012) Generating phenotypical erroneous human behavior to evaluate human–automation interaction using model checking. Int J Hum Comput Stud 70:888– 906 Heymann M, Degani A (2007) Formal analysis and automatic generation of user interfaces: approach, methodology, and an algorithm. Hum Factors 49:311–330 Clarke EM, Wing JM (1996) Formal methods: state of the art and future directions. ACM Comput Surv (CSUR) 28:626–643
Int J Adv Manuf Technol (2018) 98:1505–1521 22. 23.
24.
25.
26.
27.
28. 29.
30.
31. 32.
33.
34.
Ramadge PJ, Wonham WM (1987) Supervisory control of a class of discrete event processes. SIAM J Control Optim 25:206–230 Naylor AW, Maletz MC (1986) The manufacturing game: a formal approach to manufacturing software. Syst Man Cybern IEEE Trans 16:321–334 Negri E, Fumagalli L, Garetti M, Tanca L (2016) Requirements and languages for the semantic representation of manufacturing systems. Comput Ind 81:55–66 Jong W-R, Lai P-J, Chen Y-W, Ting Y-H (2015) Automatic process planning of mold components with integration of feature recognition and group technology. Int J Adv Manuf Technol 78:807–824 Bolton ML, Bass EJ (2013) Generating erroneous human behavior from strategic knowledge in task models and evaluating its impact on system safety with model checking. IEEE Transactions on Systems, Man, and Cybernetics: Systems 43:1314–1327 Li M, Molinaro K, Bolton ML (2015) Learning formal humanmachine interface designs from task analytic models, in Proceedings of the Human Factors and Ergonomics Society Annual Meeting, pp. 652–656 Rushby J (2014) The Versatile Synchronous Observer, in Specification, Algebra, and Software, pp. 110–128 Luo Y, Zhang L, Tao F, Ren L, Liu Y, Zhang Z (2013) A modeling and description method of multidimensional information for manufacturing capability in cloud manufacturing system. Int J Adv Manuf Technol 69:961–975 Campos JC, Doherty G, Harrison MD (2014) Analysing interactive devices based on information resource constraints. Int J Hum Comput Stud 72:284–297 Degani A, Heymann M (2002) Formal verification of humanautomation interaction. Hum Factors 44:28–43 Zhang Y, Luo X, Zhang B, Zhang S (2017) Semantic approach to the automatic recognition of machining features. Int J Adv Manuf Technol 89:417–437 Bolton ML, Bass EJ (2013) Evaluating human-human communication protocols with miscommunication generation and model checking, in NASA Formal Methods Symposium, pp 48–62 Bolton ML, Bass EJ (2012) Using model checking to explore checklist-guided pilot behavior. Int J Aviat Psychol 22:343–366
1521 35.
Wang T, Guo S, Lee C-G (2014) Manufacturing task semantic modeling and description in cloud manufacturing system. Int J Adv Manuf Technol 71:2017–2031 36. Castillo I, Smith JS (2002) Formal modeling methodologies for control of manufacturing cells: survey and comparison. J Manuf Syst 21:40–57 37. Brok R, Haugen Ø (1993) Engineering real-time systems, ed. Prentice Hall 38. Halbwachs N (1992) Synchronous programming of reactive systems. Springer Science & Business Media 39. Zhang Y-D, Yang Z-J, Lu H-M, Zhou X-X, Phillips P, Liu Q-M, Wang SH (2016) Facial emotion recognition based on biorthogonal wavelet entropy, fuzzy support vector machine, and stratified cross validation. IEEE Access 4:8375–8385 40. Hierons RM (1997) Testing from a Z specification. Software Testing Verification Reliability 7:19–33 41. Johnston W (1996) A type checker for Object-Z 42. Manna Z, Waldinger RJ (1971) Toward automatic program synthesis. Commun ACM 14:151–165 43. Sadeghipour S, Singh H (1998) Test strategies on the basis of extended finite state machines, in Daimler-Benz AG, Research and Technology 44. Lano K (1997) Specifying reactive systems in B AMN, ZUM'97: The Z Formal Specification Notation, pp. 242–274 45. Broy M, Wirsing M (2000) Algebraic state machines, in algebraic methodology and Software Technology, ed. Springer, pp 89–118 46. Kuehlmann A and Bergamaschi R (1992) High-level state machine specification and synthesis, in Computer Design: VLSI in Computers and Processors, ICCD'92. Proceedings, IEEE 1992 International Conference on, 1992, pp. 536–539 47. Duke R, King P, Rose G, Smith G (1991) The Object-Z specification language: Version 1 48. Bolton ML, Siminiceanu RI, Bass EJ (2011) A systematic approach to model checking human–automation interaction using task analytic models. IEEE Trans Syst Man Cybern Syst Hum 41:961–976 49. De Moura L, Owre S, Shankar N (2003) The SAL language manual, Computer Science Laboratory, SRI International, Menlo Park, Tech. Rep. CSL-01-01
