[go: up one dir, main page]

CN107817970B - Component system modeling and dynamic evolution consistency verification method thereof - Google Patents

Component system modeling and dynamic evolution consistency verification method thereof Download PDF

Info

Publication number
CN107817970B
CN107817970B CN201710990872.0A CN201710990872A CN107817970B CN 107817970 B CN107817970 B CN 107817970B CN 201710990872 A CN201710990872 A CN 201710990872A CN 107817970 B CN107817970 B CN 107817970B
Authority
CN
China
Prior art keywords
component system
component
evolution
state
behaviors
Prior art date
Legal status (The legal status is an assumption and is not a legal conclusion. Google has not performed a legal analysis and makes no representation as to the accuracy of the status listed.)
Expired - Fee Related
Application number
CN201710990872.0A
Other languages
Chinese (zh)
Other versions
CN107817970A (en
Inventor
李彤
郑明�
林英
谢仲文
秦江龙
莫启
周小煊
李响
明利
郑交交
杨真谛
王晓芳
成蕾
Current Assignee (The listed assignees may be inaccurate. Google has not performed a legal analysis and makes no representation or warranty as to the accuracy of the list.)
Yunnan University YNU
Original Assignee
Yunnan University YNU
Priority date (The priority date is an assumption and is not a legal conclusion. Google has not performed a legal analysis and makes no representation as to the accuracy of the date listed.)
Filing date
Publication date
Application filed by Yunnan University YNU filed Critical Yunnan University YNU
Priority to CN201710990872.0A priority Critical patent/CN107817970B/en
Publication of CN107817970A publication Critical patent/CN107817970A/en
Application granted granted Critical
Publication of CN107817970B publication Critical patent/CN107817970B/en
Expired - Fee Related legal-status Critical Current
Anticipated expiration legal-status Critical

Links

Images

Classifications

    • G—PHYSICS
    • G06—COMPUTING OR CALCULATING; COUNTING
    • G06F—ELECTRIC DIGITAL DATA PROCESSING
    • G06F8/00—Arrangements for software engineering
    • G06F8/20—Software design
    • G06F8/22—Procedural
    • G—PHYSICS
    • G06—COMPUTING OR CALCULATING; COUNTING
    • G06F—ELECTRIC DIGITAL DATA PROCESSING
    • G06F11/00—Error detection; Error correction; Monitoring
    • G06F11/36—Prevention of errors by analysis, debugging or testing of software
    • G06F11/3604—Analysis of software for verifying properties of programs
    • G06F11/3608—Analysis of software for verifying properties of programs using formal methods, e.g. model checking, abstract interpretation

Landscapes

  • Engineering & Computer Science (AREA)
  • Theoretical Computer Science (AREA)
  • Software Systems (AREA)
  • General Engineering & Computer Science (AREA)
  • Physics & Mathematics (AREA)
  • General Physics & Mathematics (AREA)
  • Computer Hardware Design (AREA)
  • Quality & Reliability (AREA)
  • Management, Administration, Business Operations System, And Electronic Commerce (AREA)

Abstract

The invention belongs to the technical field of software development, and discloses a component system modeling and dynamic evolution consistency verification method thereof, wherein a component model is constructed by applying process algebra, and a coarse-grained component system is obtained on the basis; extracting external behaviors of the component system according to the change of the component system and the state of the component system, and defining a dynamic evolution consistency verification criterion of the component system based on a weak mutual simulation theory; and extracting the behaviors of the component system before and after evolution, and converting the behaviors into a format convenient for the Pi calculation automatic tool MWB to identify so as to carry out behavior consistency verification. According to the invention, a component system with coarser granularity and convenient for behavior consistency analysis before and after evolution is constructed based on interaction and combination relation among components; an external behavior sequence extraction algorithm of the component system is provided, so that the automation of the external behavior sequence extraction of the component system is realized; a verification criterion of behavior consistency before and after component system evolution is provided based on a Milner weak mutual simulation theory.

Description

Component system modeling and dynamic evolution consistency verification method thereof
Technical Field
The invention belongs to the technical field of software development, and particularly relates to a component system modeling and dynamic evolution consistency verification method thereof.
Background
With the development of software development technology, the software development method based on the component type is relatively mature. In general, component-based software engineering (CBSE) is a system that assembles required components into a final required system through integration. With the maintenance of the system and the change of user requirements, the addition, deletion and modification of components cannot be avoided, and whether the behavior of the component system after evolution deviates from the behavior of the component system before evolution is an essential standard for judging whether the dynamic evolution of the component system is correct or not, and is also an important condition for ensuring the implementation reliability of the dynamic evolution, namely that the observable interactive behaviors between the component and other components must be kept consistent before and after the dynamic evolution.
In order to verify the system consistency problem before and after the evolution of the software system, domestic and foreign scholars perform a great deal of analysis work aiming at the component modeling facing the dynamic evolution and the verification of the system behavior consistency before and after the evolution. For example, the document provides the necessary condition for replacing components in a component-based software system based on a component behavior protocol, and as for whether the replaced component system is consistent with the component system before replacement, the author does not provide a corresponding method for verifying the consistency of the system before and after replacement, so that the invention provides a method for verifying the consistency of evolution of the component system before and after replacement based on process algebra modeling. The document models the component based on a Petri net formalization tool and adds consistency constraint on a system behavior layer, so that the flexibility is increased on the premise of ensuring the correct function and behavior of the original system, but the document does not have the standard concurrent operation of combining a plurality of Petri subnet component behaviors into a large Petri net component system behavior in a calculation mode, so that the consistency standard before and after component evolution is lower, and the consistency of the system after evolution is difficult to be accurately verified. The method comprises the steps of building a component model based on process algebra, formally describing a component and an external interaction protocol thereof, giving a verification rule of behavior consistency before and after evolution, but lacking extraction of external interaction behavior of the component and a specific standard of the consistency of the component behavior, and therefore the invention provides an extraction algorithm of external behavior sequences of a component system model and a consistency verification criterion based on a weak mutual simulation theory. The literature models the behavior of the state before and after software evolution based on a time automata model, and utilizes a time automata model verification tool UPPAAL to verify the safety protocol and the activity protocol of the system, but the time automata cannot finely depict the activities in the component system, such as the concurrent execution of a plurality of activities cannot be effectively described, and the like. The invention adopts the process algebra to model the component just because the process algebra can effectively support the concurrency of a plurality of activities in the component system, and can calculate and combine the behaviors of a plurality of components into a total behavior, and supports the analysis of similarity on the theory of weak mutual simulation, thereby supporting the verification of the consistency before and after the dynamic evolution of the component system.
In summary, the problems of the prior art are as follows: aiming at the problem of consistency maintenance of a component system after dynamic evolution, a generally accepted standard is not available at present, the invention provides a behavior consistency standard before and after dynamic evolution of the component system based on a Milner weak mutual simulation theory, and provides an extraction algorithm of an external behavior sequence of a component system model for the aspect of behavior extraction of the component system, so that the automation of the extraction of the external behavior sequence of the component system model is realized.
Disclosure of Invention
Aiming at the problems in the prior art, the invention provides a component system modeling and dynamic evolution consistency verification method thereof.
The invention is realized in such a way that a component system modeling and dynamic evolution consistency verification method thereof comprises the following steps:
constructing a component model by applying process algebra, and obtaining a component system with coarse granularity on the basis of the constructed component model; extracting external behaviors of the component system according to the component system and the change of the state of the component system; defining a component system dynamic evolution consistency verification criterion based on a weak mutual simulation theory; and extracting the behaviors of the component system before and after evolution, converting the behaviors into a format convenient for the Pi calculation automatic tool MWB to identify, and verifying the consistency of the behaviors.
Further, the component model comprises a request service interface and a provide service interface; the number of the interfaces of the component model is k, wherein k is more than or equal to 0 and less than or equal to n, and the interfaces of the component model have the internal connection relationship from a service interface to a request interface and from the request interface to another request interface;
the coarse-grained component system comprises:
the component system is a quadruplet:
Figure BDA0001441453760000031
wherein:
NM：NMname of the component system;
Figure BDA0001441453760000032
is a collection of component objects;
LM: representing a finite external connection set of components, and embodying assembly connection information between the components in a component system, wherein each pair of component connections li∈LMDefining a triple li＝<CN,Itei,LCi>Wherein, in the step (A),
CN: a component model name in the connection relationship;
Itei：
Figure BDA0001441453760000033
representing an interface between connected component models;
LCi is as follows: indicating member CNA component connected to the component system;
for two connected members
Figure BDA0001441453760000034
And
Figure BDA0001441453760000035
Figure BDA0001441453760000036
if C is presentiRequest call CjProviding a service interface, it, such an it may be referred to as CiAnd CjShared request/service interface of (1), using e (C)i,Cj) It is shown that the corresponding inter-component interface method operation set is a (C)i,Cj) It means that the method operations in the interface Ite are actions that need to be performed simultaneously, i.e., synchronization of the interface method operation actions.
SM：SMIndicating the state of the component system, SM＝{s1,s2,…,sn}(si∈SCi,0≤i≤n)，SInitTo initialize the state, SFinaIs in the end state.
Further, the extracting of the component system external behavior comprises:
firstly, taking the nodes of the Graph as state nodes of the component system, wherein the nodes comprise an initial state node (Start) and an End state node (End), and the edges among the nodes of the Graph are actions for causing state transition;
initializing graph and stacking an initial state node Start;
entering a while loop, and in the loop, checking whether a stack top state node s has a state node which can be reached, is not stacked and is not accessed from the node s (judged by using an AdjUnvisitedVertex function) in the Graph; if yes, the found state node is pushed; if not, popping up a stack top state node s, printing and outputting the elements in the stack when the stack top element is in the end point state, and popping up the stack top state node;
the While loop is repeatedly executed until the stack is empty, and all action sequences (i.e., external behaviors of the component system) in the Graph from the start state node to the end state node are found.
Further, in the definition of the verification criterion of the dynamic evolution consistency of the component system based on the weak mutual simulation theory, the weak mutual simulation comprises:
some binary relationship B on PA is a weak inter-analog relationship if and only if: whenever, if there is (E)1,E2) E, B, then for all operations the following two conditions are satisfied simultaneously:
(1) if it is
Figure BDA0001441453760000041
Then E is present2′，
Figure BDA0001441453760000042
And (E)1′,E2′)∈B；
(2) If it is
Figure BDA0001441453760000043
Then E is present1′，
Figure BDA0001441453760000044
And (E)1′,E2′)∈B；
The set of weak inter-simulation relationships is the observation equivalence relationship, denoted as E1≈BE2Wherein
Figure BDA0001441453760000045
and a represents neglecting the influence of tau in the action, and if a is tau, a is epsilon, wherein epsilon represents a null operation sequence, otherwise a is a.
Further, the converting into a format convenient for the Pi-calculus automatic tool MWB to identify includes: the method comprises the steps of firstly extracting external behaviors according to an external behavior sequence extraction algorithm of a component system, and then writing behaviors of the component system before and after evolution into a specific behavior sequence meeting an MWB format according to the format of an MWB tool.
Another object of the present invention is to provide a component system of the above component system modeling and dynamic evolution consistency verification method.
The invention has the advantages and positive effects that: on the basis of providing a component model, a component system with coarser granularity and convenient for behavior consistency analysis before and after evolution is constructed based on interaction and combination relation among components; an external behavior sequence extraction algorithm of the component system model is provided, so that the automation of the external behavior sequence extraction of the component system is realized; a verification criterion of behavior consistency before and after component system evolution is provided based on a Milner weak mutual simulation theory.
The invention has very important meanings in both theory and practice, analyzes the initially established component type software modeling theory and method supporting dynamic evolution based on process algebra from the theoretical point of view, is natural extension and expansion of the traditional software dynamic evolution under a formalization method, has important theoretical significance for formalization modeling of a software system, and also provides a new idea and method for consistency research of the software system before and after dynamic evolution. From the practical significance, the consistency verification method provided by the invention is beneficial to improving the effectiveness of the dynamic evolution of the software system based on the component, simultaneously reduces the cost for verifying the consistency of the dynamic evolution of the software system based on the component development, and finally further improves the quality and the efficiency of the dynamic evolution implementation scheme of the software system based on the component development.
Drawings
Fig. 1 is a flowchart of a component system modeling and dynamic evolution consistency verification method thereof according to an embodiment of the present invention.
Fig. 2 is a block diagram of a method for verifying consistency of dynamic evolution of a component system according to an embodiment of the present invention.
FIG. 3 is a diagram of a component model according to an embodiment of the present invention.
In the figure:
Figure BDA0001441453760000051
service interfaces (number n, n is 1, 2 …, n);
Figure BDA0001441453760000052
request interfaces (number n, n is 1, 2 …, n);
Figure BDA0001441453760000053
internal connections (number n, n ═ 1, 2 …, n)
Fig. 4 is a system diagram of an online train ticket booking component provided by the embodiment of the invention.
Fig. 5 is a state transition diagram (partial) of an evolutionary pre-component system provided by an embodiment of the present invention.
Fig. 6 is a component system state transition diagram (part) after the evolution of the first evolution scheme provided by the embodiment of the present invention.
Fig. 7 is a component system state transition diagram (part) after the evolution of the second evolution scheme provided by the embodiment of the present invention.
FIG. 8 is an evolution front-component system external behavior process algebraic expression.
FIG. 9 is an algebraic expression of external behavior process of a component system after the evolution of the first evolution mode.
FIG. 10 is a component system external behavior process algebraic expression after the evolution of the second evolution mode.
Detailed Description
In order to make the objects, technical solutions and advantages of the present invention more apparent, the present invention is further described in detail with reference to the following embodiments. It should be understood that the specific embodiments described herein are merely illustrative of the invention and are not intended to limit the invention.
The application of the principles of the present invention will now be further described with reference to the accompanying drawings.
As shown in fig. 1, the component system modeling and dynamic evolution consistency verification method provided in the embodiment of the present invention includes the following steps:
s101, constructing a component model by applying a process algebra, and obtaining a component system with coarse granularity on the basis;
s102, according to the change of the component system and the state of the component system, providing an external behavior extraction algorithm of the component system, and defining a dynamic evolution consistency verification criterion of the component system based on a weak mutual simulation theory;
s103, extracting the behaviors of the component system before and after evolution, and converting the behaviors into a format which is convenient for a Pi calculation automatic tool MWB (mobility workbench) to identify so as to carry out behavior consistency verification.
As shown in fig. 2, a block diagram of a component system modeling and a dynamic evolution consistency verification method thereof provided by the embodiment of the present invention is shown.
The component modeling method provided by the embodiment of the invention comprises the following steps:
the behavior protocol is introduced into a component model, and the compatibility of request/service interfaces among components is deeply analyzed. The invention introduces the concept of a component system based on the existing analysis foundation, and assembles a plurality of components into the component system through the connection relationship among the components, so that the verification of the dynamic evolution consistency of the components is not based on one local component any more, but the overall verification of the component system formed by a plurality of components. The model of the components used for assembly is shown in figure 3 below. The interfaces are of two types, a request service interface and a provide service interface. The number of the interfaces of the component is k (k is more than or equal to 0 and less than or equal to n), and the internal connection relationship from the service interface to the request interface and from the request interface to the request interface exists.
Definition 1 (member): the building block is such a six tuple: c ═<Nc,IcP,IcR,ILc,Ac,Pc>Wherein:
(1) nc: name representing the component, i.e. a unique identification of the component;
(2)IcP: set of interfaces, Ic, representing the external servicing of the component CP＝{Ite1,Ite2,…ItenAny one of the interfaces Itei∈IcPService interface for representing a component to be invoked by the outside world, comprising a set of service providing interface method operations Itei＝{a1i,a2i…ani i}；
(3)IcR: set of interfaces representing the external request service of the component C, any one of which is an Itej∈IcRRepresenting the required request interface for the component, it contains a group of request call interface method operations Itej ═ { a1j,a2j…anjj}；
(4)ILC: indicating the internal connection of the components. Each member being interconnected by ili∈ILCFormalized definition of ili＝<Itei,Itej>Wherein, iti∈ICP∧ICR，Itej∈ICRIte of scaleiFor internal request interfaces, ItejIs an internal service interface. One case is where the component is a response service interface, IteiThe received request is thus passed through the request interface itjSending new requests to other components; another case is that the component is a response request interface IteiRequest results returned by other components to go through interface ItejSending new requests to other components;
(5) ac: representing a finite set of interface actions for a building block. Including service, demand and internal action sets, respectively with AcP，AcR，AcHThe three are not intersected with each other;
(6) pc: a behavior protocol representing a building block, the protocol being formally defined by PA, describing protocol constraints and specifications of the external interaction behavior of the building block, Pc corresponding to a binary < Sc, Tc > in which:
a) and (C) Sc: non-empty finite set of states, S, representing component interaction behaviorInitIs in an initial state, SFinaIs in a termination state;
b) tc: the finite state transition set representing the component external interaction behavior can be represented by a ternary formula (s, a, s ') ∈ TC, wherein s, s ' belongs to Sc, and a belongs to Ac, and is recorded as a state, and the finite state transition set represents the component external interaction behavior state to be converted from the state s to the state s ' under the action a; member C in the present invention does not have such a case: that is, (s, a, s ') and (s, a, s ') exist simultaneously, where s, s ' belongs to Sc, a belongs to Ac, s ' ≠ s '.
The parallel combination operator "|", in the process algebra, is used for describing from the behavior of several concurrent interactive subsystems, calculate and get the total behavior that they combine together, therefore, in the definition and description about external connection set and behavior agreement of the component, can give the behavior description after a plurality of components are combined with this inference rule, and then combine the execution semanteme of the component system and can get the state transition relation of the component system. Therefore, a component system assembled from a plurality of components is defined as follows, wherein the execution semantics of the component system are included.
The component system modeling method provided by the invention comprises the following steps:
definition 2 (component system): the building block system is a quadruple of: m ═<NM,CM Set,LM,SM>Wherein:
(1)NM：NMname of the component system;
(2)CM Set：CM Set＝{C|C＝<Nc,IcP,IcR,ILc,Ac,Pc>is a set of member objects;
(3)LM: representing a finite component external connection set, and embodying the assembly connection information between components in a component system, wherein each pair of component connections li belongs to the LMDefine the following triplet li ═<CN,Itei,LCi>Wherein:
a)CN: a component name in a connection relationship;
b)Itei：Itei∈IcP∧IcRrepresenting an interface between connected components;
LCi: indicating member CNAnd a member c) connected to the member system.
For two connected members Ci＝<Nci,Ici P,Ici R,ILci,Aci,Pci>And Cj＝<Ncj,Icj P,Icj R,ILcj,Acj,Pcj>If C is presentiRequest call CjProviding a service interface, it, such an it may be referred to as CiAnd CjIs denoted by e (Ci, Cj), and the corresponding inter-component interface method operation set is a (C)i,Cj) It means that the method operations in the interface Ite are actions that need to be performed simultaneously, i.e., synchronization of the interface method operation actions.
(4)SM：SMIndicating the state of the component system, SM＝{s1,s2,…,sn}(si∈Sci,0≤i≤n)，SInitTo initialize the state, SFinaIs in the end state.
Definition 3 (execution semantics of a component system) let S and S' be two different states of a component system, where S ═ { S ═ S1,s2,…,sn},S’＝{s’1,s’2,…,s’nThat the state of the component system can be transferred from state S to state S' by action a when one of the following two conditions is fulfilled.
a) Having action a ∈ AHciAnd(s)i,a,si') E Tci, and simultaneously, C for other components in the component systemj(j is not less than 1 and not more than n, j is not equal to i) is sj＝s’j；
b) There are actions a ∈ Ite, Ite ∈ e (C)i,Cj) (1. ltoreq. i, j. ltoreq. n, i. not equal to j), if (si, a, si') ∈ TciAnd(s)j,a,sj’)∈TcjAt the same time, for other components C in the component systemk(1. ltoreq. k.ltoreq.n, k.noteq.i.noteq.j) with sk＝s’k。
The invention provides an external behavior process algebraic expression form extraction algorithm of a component system, which comprises the following steps:
for the purpose of extracting the external behavior process algebraic expression form of the component system based on the depth-first traversal algorithm, the external behavior process algebraic expression form extraction algorithm of the component system is provided, and the external behavior process algebraic expression form extraction algorithm of the component system is as follows:
algorithm 1, extracting an algorithm in the form of an algebraic expression of an external behavior process of a component system.
Figure BDA0001441453760000091
Figure BDA0001441453760000101
The algorithm 1 is an extraction algorithm of the algebraic expression form of the external behavior process of the component system. Before executing the algorithm, the action sequence of the component system state and the state transition is represented by Graph, wherein the nodes of the Graph are the state nodes of the component system, the nodes comprise an initial state node number (Start) and an End state node number (End), and the edges between the nodes of the Graph are the actions causing the state transition. The algorithm first initializes the graph and pushes the initial state Start onto the stack. The algorithm then enters a while loop in which the top-of-stack state node s is looked at for state nodes in the graph that are not reachable, not stacked, and not visited from this node s (as determined by the adjuvisitedvertex function). If so, the found state node is pushed. And if not, popping up a stack top state node s, printing and outputting the elements in the stack when the stack top element is in the end point state, and popping up the stack top state node. The While loop is repeatedly executed until the stack is empty, and all action sequences (i.e., external behaviors of the component system) in the graph from the start state node to the end state node have been found.
The consistency verification criterion before and after the dynamic evolution of the component system provided by the invention is as follows:
the invention provides a verification criterion of the evolution consistency of a component system from the perspective of external behaviors. Since the behavior protocol describes the observation of the component behavior from the outside of the component, when the component is evolved, if the evolved component still satisfies the behavior specified by the user in the whole component system, the evolved component does not have a great difference before and after the evolution even though the implementation manner before and after the evolution is changed greatly from the observation of the outside of the component. It can be seen that the key to maintaining consistency of external behaviors is that the evolved component system can still "simulate" the behaviors required by the user. Since the interior of a component within a component system is not observable, this "simulation" is a "weak simulation" that requires from an external perspective, focusing only on externally observable "external behavior" and not externally observable "internal behavior".
Defining a certain binary relation B on 4 (weak cross-simulation) PA as a weak cross-simulation relation, if and only if: whenever, if there is (E)1，E2) E, B, then for all operations the following two conditions are satisfied simultaneously:
(1) if it is
Figure BDA0001441453760000111
Then E is present2′，
Figure BDA0001441453760000112
And (E)1′，E2′)∈B；
(2) If it is
Figure BDA0001441453760000113
Then E is present1′，
Figure BDA0001441453760000114
And (E)1′，E2′)∈B。
The set of weak inter-simulation relationships are observed equivalent (observationequivalences) relationshipsIs, can be represented as E1≈BE2Wherein
Figure BDA0001441453760000115
This indicates that the influence of τ in the operation is ignored, that is, if a is τ, then
Figure BDA0001441453760000116
Here, ε represents a sequence of no-operation, otherwise
Figure BDA0001441453760000117
The component evolution inside the component system leads to the evolution of the component system, if the external behavior of the component system before the evolution is equivalent to the external behavior of the component system after the evolution, and the external behavior of the component system is calculated and combined by a plurality of external behaviors of the components in the component system, the component system M after the evolution can be ensuredevolutionThe evolved component can be compatible with interaction between components which are not evolved in the component system M, namely, external behaviors embodied by the evolved component have no difference to users, so that functions embodied by the whole evolved component system have no difference, and a criterion of behavior consistency of the component system before and after evolution is obtained.
Consistency verification criteria (component systems) if external behavior of component system M before evolution and component system M after evolutionevolutionThe external behaviors of the two component systems are equivalent, that is, the component system after evolution and the component system before evolution satisfy a consistency relationship, and is recorded as M-Mevolution。
The component system based on component combination is dynamically evolved, wherein the dynamic evolution of one component can lead to the evolution of the whole component system ifExternal behavior of component system M before evolution and component system M after evolutionevolutionThe external behaviors satisfy definition 4, that is, a weak mutual simulation relationship exists between them, so that the external behaviors of the component system before and after evolution are equivalent, that is, the interaction behaviors between the component in the component system after evolution and other components in the original component system are compatible, and consistency maintenance is satisfied, so that it can be ensured that the component system after evolution and the component system before evolution satisfy the consistency definition, that is, M is Mevolution。
1. Case analysis
1.1 component system modeling of online train booking
In order to verify that the consistency verification method before and after component system evolution is really feasible and effective, a classical online application system is used: the online train booking component system is specifically described by taking an example. When a Train is ordered using a network, nine types of components participate in a component System (OTTBS) in which Online Train ordering is composed, as shown in fig. 4 below.
The method comprises the following steps: user view (UserView), controller (ControllerCenter), user registration (register), user Login (Login), information query (InfoSearch), ticket reservation (TicketBook), refund and change sign (tickegchange), DataBase (DataBase), and banking system (Bank). The whole system operates roughly as follows: the user can acquire the information of the train through the information inquiry component without registering, but if the ticket is scheduled or the ticket is refunded and changed, the user can use the related component function only after registering and logging in. After the user logs in and selects the ticket booking or refunding and changing service, the ControllerCenter component requests the component Bank to complete the online payment or refunding operation of the user. When the user needs to use the ticket refunding or ticket changing function, the TicketChange component requests the component controllerCenter to inquire the information of the existing tickets of the user, wherein the component register, the component Login, the component InfoSearch, the component TicketBook and the TicketChange need to request to call and interact with the DataBase component DataBase of the railway company in real time.
As known from online train ticketing component systems on the internet, the entire component system has fifteen external connections, among which, the component ControllerCenter responds to a request received from a service interface itecondroller _ User, so as to send new requests to the component register, the component InfoSearch and the component Login through interfaces itecondntroller _ register, itecondntroller _ InfoSearch and itecondntroller _ Login, respectively, so that there are internal connections < itecondntroller _ User, itecondntroller _ register >, < itecondontroller _ User, itecondontroller _ InfoSearch >, and < itecondontroller _ er, econtroller _ Login >; component register, component InfoSearch, and component Login are responsive to requests received from service interfaces itecondroller _ register, itecondroller _ InfoSearch, and itecondroller _ Login to send new requests to component DataBase over interfaces itecondroller _ Data, itenfonsearch _ Data, and IteLogin _ Data, respectively, so there are internal connections < itecondroller _ register, itecondensor _ Data >, < itecondroller _ InfoSearch, itenfosearch _ Data >, and < itecondroller _ Login, itecondensor _ Data >. When a user logs in and needs to use a ticketing service, the component ControllerCenter sends a new request to the component tickettoook through the interface itecondntroller _ ticket in response to a ticketing request received from the service interface iteconderterclercenterloggin, so that there are internal connections < itecondntroller center _ Login, itecondntroller _ ticket >, the component tickettook sends a car-order information query request and a request withholding request, respectively, through the interface iteconderterboook _ Data and the interface itecondetrolercentercounterkey, the component controllercenterc sends a new request to the component tickettoook through the interface itecondensor, the component controllerceokouk in response to a withholding request received from the service interface itecondertercontroller _ ticket interface, the component control _ ticket, so that there are internal connections < itecondensor _ control _ ticket, and the component; similarly, if the user needs to use the ticket refund or change sign service, there are internal connections < IteControlerCenter _ Login, IteControler _ TicketChange >, < IteControler _ TicketChange, IteControlerCenter _ TicketChange >, < IteControler _ TicketChange, IteTicketChange _ Data >, and < IteControlerCenter _ TicketChange, IteControler _ Bank >.
1.2 Member System Formal description and consistency verification for Online train Ticket booking on the Internet
For the sake of brevity, only the component ControllerCenter and the component Bank are described herein in accordance with definition 1, as follows:
the component ControllerCenter is described as follows:
Figure BDA0001441453760000141
Figure BDA0001441453760000151
Figure BDA0001441453760000161
the description of the building blocks Bank is as follows:
Figure BDA0001441453760000162
Figure BDA0001441453760000171
according to the definition of the component System in definition 2, an Online Train Booking component System (OTTBS) is described as follows:
Figure BDA0001441453760000172
Figure BDA0001441453760000181
the state transition diagram of OTTBS is obtained according to OTTBS and in combination with the execution semantics in definition 3 as shown in fig. 5:
as the Bank system is upgraded, the dynamic evolution of the component Bank is needed, namely, a user credit mechanism is added: the component Bank deducts the fare required to pay from the credit account of the user's Bank system, then does an internal action for checking whether the account balance is sufficient, and then continues to generate a corresponding Bank system notification message to the result after checking, the generated action is also an internal action, namely if the balance is sufficient or the credit account can be overdrawn, the Bank system message will be pushed to the user along with the execution of the subsequent external action buyTicket _ success; if the balance is insufficient and the credit account cannot be overdrawn, the bank system message is pushed to the user along with the execution of the subsequent external action buyTicket _ failure, and because the internal action for generating the bank system message can be two different modes of generating the bank system message by directly generating the classification message and regenerating the classification message into the classification message, the dynamic evolution mode of the component Bnak has two modes:
first evolutionary approach component Bank the evolved component EvolutionBank1 is described below (where the internal action of checking account balances is denoted τ 1 and the internal action of generating classified Bank system messages is denoted τ 2):
Figure BDA0001441453760000182
Figure BDA0001441453760000191
for the sake of space, the invention does not describe the evolved component system, and the state transition diagram of the component system OTTBSEvolution1 dynamically evolved in the first evolution mode is shown in fig. 6 below.
Second evolution means Bank the evolved means EvolutionBank2 is described below (where the internal actions of checking account balances τ 1 are denoted and the internal actions of categorically generating Bank system messages are denoted with τ 2 and τ 3):
Figure BDA0001441453760000192
Figure BDA0001441453760000201
component system OTTBSEvolume after dynamic evolution of second evolution mode2The state transition diagram is shown in fig. 7 below.
The algebraic expression form of the external behavior process of the component system before evolution and after evolution of two different dynamic evolution modes is obtained by using the component system state transition diagrams in fig. 5, 6 and 7 and the algorithm 1 as shown in fig. 8, 9 and 10.
The above description is only for the purpose of illustrating the preferred embodiments of the present invention and is not to be construed as limiting the invention, and any modifications, equivalents and improvements made within the spirit and principle of the present invention are intended to be included within the scope of the present invention.

Claims (4)

1. A component system modeling and dynamic evolution consistency verification method is characterized by comprising the following steps:
constructing a component model by applying process algebra, and obtaining a component system with coarse granularity on the basis of the constructed component model; extracting external behaviors of the component system according to the component system and the change of the state of the component system; defining a component system dynamic evolution consistency verification criterion based on a weak mutual simulation theory; extracting the behaviors of the component system before and after evolution, converting the behaviors into a format convenient for the Pi calculation automatic tool MWB to identify, and verifying the consistency of the behaviors;
the extraction of the external behaviors of the component system comprises the following steps:
firstly, taking the state of a component system and the nodes of the Graph of the action sequence of state conversion as the state nodes of the component system;
initializing Graph and stacking an initial state node Start;
entering a while loop, and in the loop, checking whether a stack top state node s arrives at the Graph, is stacked and is a state node which is not accessed from the node s; if yes, the found state node is pushed; if not, popping up a stack top state node s; when the stack top element is in the end point state, printing and outputting the element in the stack, and popping up a stack top state node;
repeatedly executing the While loop until the stack is empty, and finding all action sequences starting from the starting state node to the end state node in the Graph;
in the method for defining the verification criterion of the dynamic evolution consistency of the component system based on the weak mutual simulation theory, the weak mutual simulation comprises the following steps:
some binary relationship B on PA is a weak inter-analog relationship if and only if: whenever, if there is (E)1,E2) E, B, then for all operations the following two conditions are satisfied simultaneously:
(1) if it is
Figure FDA0003253688180000011
Then E is present2′，
Figure FDA0003253688180000012
And (E)1',E2')∈B；
(2) If it is
Figure FDA0003253688180000013
Then E is present1′，
Figure FDA0003253688180000014
And (E)1',E2')∈B；
The set of weak inter-simulation relationships is the observation equivalence relationship, denoted as E1≈BE2Wherein
Figure FDA0003253688180000021
Figure FDA0003253688180000022
This indicates that the influence of τ in the operation is ignored, and if a is τ, then
Figure FDA0003253688180000023
Where ε represents a sequence of no-operation, otherwise
Figure FDA0003253688180000024
2. The component system modeling and dynamic evolution consistency verification method as claimed in claim 1,
the component model comprises a request service interface and a provide service interface; the number of the interfaces of the component model is k, wherein k is more than or equal to 0 and less than or equal to n, and the interfaces of the component model have the internal connection relationship from a service interface to a request interface and from the request interface to another request interface;
the coarse-grained component system comprises:
the component system is a quadruplet:
Figure FDA0003253688180000025
wherein:
NM：NMname of the component system;
Figure FDA0003253688180000026
is a collection of component objects;
LM: representing a finite external connection set of components, and embodying assembly connection information between the components in a component system, wherein each pair of component connections li∈LMDefining a triple li＝<CN,Itei,LCi>Wherein, in the step (A),
CN: a component model name in the connection relationship;
Itei：
Figure FDA0003253688180000027
representing an interface between connected component models;
LCi: indicating member CNA component connected to the component system;
SM：SMindicating the state of the component system, SM＝{s1,s2,…,snIn which s isi∈SCi,0≤i≤n，SInitTo initialize the state, SFinaIs in the end state.
3. The method of component system modeling and dynamic evolution consistency verification of the same as in claim 1, wherein the converting to a format that facilitates Pi calculus automation tool MWB identification comprises: the method comprises the steps of firstly extracting external behaviors according to an external behavior sequence extraction algorithm of a component system, and then writing behaviors of the component system before and after evolution into a specific behavior sequence meeting an MWB format according to the format of an MWB tool.
4. A component system, characterized in that the component system executes the component system modeling and dynamic evolution consistency verification method as claimed in any one of claims 1 to 3.
CN201710990872.0A 2017-10-23 2017-10-23 Component system modeling and dynamic evolution consistency verification method thereof Expired - Fee Related CN107817970B (en)

Priority Applications (1)

Application Number Priority Date Filing Date Title
CN201710990872.0A CN107817970B (en) 2017-10-23 2017-10-23 Component system modeling and dynamic evolution consistency verification method thereof

Applications Claiming Priority (1)

Application Number Priority Date Filing Date Title
CN201710990872.0A CN107817970B (en) 2017-10-23 2017-10-23 Component system modeling and dynamic evolution consistency verification method thereof

Publications (2)

Publication Number Publication Date
CN107817970A CN107817970A (en) 2018-03-20
CN107817970B true CN107817970B (en) 2021-12-17

Family

ID=61608616

Family Applications (1)

Application Number Title Priority Date Filing Date
CN201710990872.0A Expired - Fee Related CN107817970B (en) 2017-10-23 2017-10-23 Component system modeling and dynamic evolution consistency verification method thereof

Country Status (1)

Country Link
CN (1) CN107817970B (en)

Families Citing this family (2)

* Cited by examiner, † Cited by third party
Publication number Priority date Publication date Assignee Title
CN111124348B (en) * 2019-12-03 2023-12-05 光禹莱特数字科技(上海)有限公司 Method and device for generating interaction engine cluster
CN112416337B (en) * 2020-11-11 2023-05-02 北京京航计算通讯研究所 Software architecture development system for aerospace embedded system

Citations (3)

* Cited by examiner, † Cited by third party
Publication number Priority date Publication date Assignee Title
CN102270130A (en) * 2011-06-27 2011-12-07 浙江工业职业技术学院 Formal description method for adaptive software architecture during operation
CN103488568A (en) * 2013-09-30 2014-01-01 南京航空航天大学 Embedded software trusted attribute modeling and verification method
CN106897396A (en) * 2017-02-07 2017-06-27 云南大学 A kind of process model mining method and system based on implicit features

Family Cites Families (1)

* Cited by examiner, † Cited by third party
Publication number Priority date Publication date Assignee Title
EP1330709A2 (en) * 2000-11-03 2003-07-30 Wilde Technologies Limited A software development process

Patent Citations (3)

* Cited by examiner, † Cited by third party
Publication number Priority date Publication date Assignee Title
CN102270130A (en) * 2011-06-27 2011-12-07 浙江工业职业技术学院 Formal description method for adaptive software architecture during operation
CN103488568A (en) * 2013-09-30 2014-01-01 南京航空航天大学 Embedded software trusted attribute modeling and verification method
CN106897396A (en) * 2017-02-07 2017-06-27 云南大学 A kind of process model mining method and system based on implicit features

Also Published As

Publication number Publication date
CN107817970A (en) 2018-03-20

Similar Documents

Publication Publication Date Title
CN110781082A (en) Method, device, medium and equipment for generating test case of interface
US20120131582A1 (en) System and Method for Real-Time Batch Account Processing
CN111680098A (en) Block chain system for data acquisition, data annotation, AI model training and verification
CN112162744A (en) A method and device for automatic code generation based on business scenarios
CN101464796A (en) Method for establishing software requirement model
CN116820714A (en) Scheduling method, device, equipment and storage medium of computing equipment
CN119356674A (en) Financial business visualization process construction method, system, equipment and medium
CN107817970B (en) Component system modeling and dynamic evolution consistency verification method thereof
CN111144139A (en) Uniqueness authentication method and identification system of translation result based on block chain
Jacob et al. An Analytical approach on DFD to UML model transformation techniques
Martens Simulation and equivalence between bpel process models
CN111061789A (en) Smart power grids capital construction information management system
CN114186267B (en) Virtual asset data processing method and device and computer readable storage medium
CN109032921A (en) A kind of structuring requirements use case automatic generation method and device
CN111125136B (en) Blockchain method and system for key term authentication in translation process
CN108647016B (en) System class structure generation method based on UML dynamic model
CN1932760B (en) System and method for execution of application program
CN110286914A (en) The implementation method of the program with life cycle based on block chain
CN115756444B (en) Construction method and system of industrial scene business center
Nguyen et al. Towards engineering product digital twins for industry 5.0: definition and modeling approach
CN120509711B (en) Data fusion-based process development methods, devices, equipment, and media
CN119295242B (en) A method, system, computer equipment and storage medium for managing current account data
CN118780924B (en) Insurance data transmission method based on big data adaptability fusion
CN120833230B (en) Fixed asset intelligent transferring method, system and electronic equipment
CN110276601A (en) E-business draft Life cycle supervisory systems and method

Legal Events

Date Code Title Description
PB01 Publication
PB01 Publication
SE01 Entry into force of request for substantive examination
SE01 Entry into force of request for substantive examination
GR01 Patent grant
GR01 Patent grant
CF01 Termination of patent right due to non-payment of annual fee
CF01 Termination of patent right due to non-payment of annual fee

Granted publication date: 20211217