Web Services Choreography Description Language lacks a formal system to accurately express the semantics of service behaviors and verify the correctness of a service choreography model.This paper presents a new approa...Web Services Choreography Description Language lacks a formal system to accurately express the semantics of service behaviors and verify the correctness of a service choreography model.This paper presents a new approach of choreography model verification based on Description Logic.A meta model of service choreography is built to provide a conceptual framework to capture the formal syntax and semantics of service choreography.Based on the framework,a set of rules and constraints are defined in Description Logic for choreography model verification.To automate model verification,the UML-based service choreography model will be transformed,by the given algorithms,into the DL-based ontology,and thus the model properties can be verified by reasoning through the ontology with the help of a popular DL reasoned.A case study is given to demonstrate applicability of the method.Furthermore,the work will be compared with other related research.展开更多
In contemporary times,with the development of multimedia technology,especially in consideration of the advantages of multimedia technology in performance,dance,as an expressive art,is bound to be concatenated with mul...In contemporary times,with the development of multimedia technology,especially in consideration of the advantages of multimedia technology in performance,dance,as an expressive art,is bound to be concatenated with multimedia technology to enrich its form of display.The influence of multimedia technology in dance choreography on dance works and the effect of multimedia technology itself on dance choreography are worth further discussion.There is no doubt that with the application of multimedia technology in the dance field,choreographers have more open and creative ideas.Perhaps,in view of the role of multimedia technology in dance creation,the involvement of various disciplines and different technologies in dance choreography would expand in the future.However,it is necessary to consider the integration of new technologies,especially the negative impact of their improper use on the expression of dance works.Therefore,this study aims to explore the elements and relations between multimedia technology and dance choreography in the new era,seek for methods and rules of multimedia technology in dance creation,pursue its positive significance,and provide certain theoretical reference for the creation of dance works through multimedia technology.展开更多
In this paper, we give a short proof for the existence of nontrivial choreography solution to the equal-mass three-body problem, which is discovered by Chenciner and Montgomery recently.
Web service choreography describes global mod- els of service interactions among a set of participants. For an interaction to be executed, the participants must know the required channel（s） used in the interaction, ...Web service choreography describes global mod- els of service interactions among a set of participants. For an interaction to be executed, the participants must know the required channel（s） used in the interaction, otherwise the ex- ecution will get stuck. Since channels are composed dynami- cally, the initial channel set of each participant is often insuf- ficient to meet the requirements. It is the responsibility of the participants to pass required channels owned （known） by one to others. Since service choreography may involve many par- ticipants and complex channel constraints, it is hard for de- signers to specify channel passing in a choreography exactly as required. We address the problem of checking whether a service choreography lacks channels or has redundant chan- nels, and how to automatically generate channel passing based on interaction flows of the service choreography in the case of channel absence. Concretely, we propose a sim- ple language Chorc, a channel interaction sub-language for modeling the channel passing aspect of service choreography. Based on the formal operational semantics of Chore, the algo- rithms for static checking of service choreography and gen- erating channel passing are also studied, and the complexity results of algorithms are discussed. Moreover, some illus- trated service choreography examples are presented to show how to formalize and analyze service choreography with channel passing in Chorc.展开更多
In order to formally reason and verify web services composition described by web services choreography specification WS-CDL,a typed formal model named typed Abstract WS-CDL（web services choreography description langu...In order to formally reason and verify web services composition described by web services choreography specification WS-CDL,a typed formal model named typed Abstract WS-CDL（web services choreography description language）for WS-CDL specifications is proposed.In typed Abstract WS-CDL,the syntax of type and session,typing rules and operational semantics are formalized;the collaborations of web services are formally described by sessions;the operational semantics of a session can help to formally reason the execution of the choreography;the typing rules can help to formally check the data type consistency of exchanged information between web services and capture run-time errors due to type mismatches.Particularly,the concepts of type assumption set extension and type assumption set compatibility are proposed,and the merging algorithm of type assumption sets is defined so as to eliminate type assumption conflict.Based on the formal model,typed mapping rules for mapping web services choreography to orchestration is also defined.With the typed mapping rules,orchestration stubs and their type assumption sets can be generated from a given choreography; thus, web services composition can be verified at choreography and orchestration levels,respectively.The model is proved to have properties of type safety,and how the model can help to reason and verify web services composition is illustrated through a case study.展开更多
Discrete manufacturing workshops are confronted with problems of processing diverse products and strict real time requirements for data service calculation and manufacturing equipment,which makes it difficult to provi...Discrete manufacturing workshops are confronted with problems of processing diverse products and strict real time requirements for data service calculation and manufacturing equipment,which makes it difficult to provide real time feedback and compensation.In this study,a high-availability,high-performance,and high-concurrency digital twin reference model was constructed to satisfy a large number of manufacturing requirements.A multiterminal real-time interaction model and information aging classification rules for virtual and physical models were established.Moreover,a multiterminal virtual interaction model was proposed,and a generalized distributed computing service digital twinning system was developed.This digital twin system was considered a machine tool box processing line as an actual case.Consequently,a full closed-loop manufacturing process digital twin platform for physical request service,real-time response,and quality information feedback from iterations,which provides case guidance for subsequent factory digital twin systems,was realized.The proposed system can satisfy the requirements of multidevice big data computing services in modern manufacturing plants,as well as multiplatform,low-latency,and high-fidelity information visualization requirements for managers.Thus,this system is expected to play an important role in information factories.展开更多
One of the most intellectually challenging and perhaps rewarding engagements in any creative endeavour, be it written literature or performance, is decrypting the metaphorical construct imbued in such a work, within t...One of the most intellectually challenging and perhaps rewarding engagements in any creative endeavour, be it written literature or performance, is decrypting the metaphorical construct imbued in such a work, within the confines of the intentions of the writer or performer. Beyond coded speech, dance and choreography are works of art which make use of symbols to communicate man＇s thought, experience, and emotions. These symbols are conveyed basically through movement and they are forms of artistic expression to which all men, across climes, can respond, be it in a live performance or recorded video film. More than ever before, the music video film has taken a great place of prominence in the entertainment circles the world over, and musical choreography has become a major tool, used by singers, musicians, and music producers in these video films to enhance their creative output and make their productions more appealing both for economic and aesthetic purposes. This paper examines the motifs of dance and choreography in two Nigerian music videos, namely, Olori Oko （2006） by a Gospel group called Infinity and Roll It （2007） by a hip-hop group named P. Sqanre. The paper investigates the themes of the music, the concepts of the dances, and the styles of choreography in both works. The paper concludes that though both works belong to different genres, they are each successful in their own rights and have both contributed in elevating the standards in the practice of dance and choreography in Nigerian music video film.展开更多
The Dikopelo music practice involves vocal singing and dancing in a patterned choreography without musical instruments in which people from a particular area join together to sing as a choir.The element is practiced b...The Dikopelo music practice involves vocal singing and dancing in a patterned choreography without musical instruments in which people from a particular area join together to sing as a choir.The element is practiced by men,women and children but is mostly dominated by the elders who, forming an informal council of advisors,transmit their skills to the younger generation.展开更多
As a disruptive technology,the blockchain is continuously finding novel application contexts,bringing new opportunities and radical changes.In this paper,we use blockchain as a communication infrastructure to support ...As a disruptive technology,the blockchain is continuously finding novel application contexts,bringing new opportunities and radical changes.In this paper,we use blockchain as a communication infrastructure to support multi-party business processes.In particular,through smart contracts specifically generated by the mentioned business process,it is possible to derive a trustable infrastructure enabling the interaction among parties.Moreover,the emergence of different blockchain technologies,satisfying different characteristics,gives the possibility to support the same business process dealing with different non-functional needs.In this paper,we propose a novel engineering methodology supported by a practical framework called Multi-Chain.It permits to derive,using a model-driven strategy,a blockchain-based infrastructure,that can be deployed over a specific blockchain technology(e.g.,Ethereum or Hyperledger Fabric).The objective is to permit the single definition and multiple deployments of the business process,to deliver the same functionalities,but satisfying different nonfunctional needs.In such a way,organisations willing to cooperate can select the multi-party business process and the blockchain technology they would like to use to satisfy their needs.Using Multi-Chain,they will be able to automatically derive from a Business Process Modelling Notation(BPMN)choreography diagram a blockchain infrastructure ready to be used.This overcomes the need to get acquainted with many details of the specific technology.展开更多
基金This work is supported by the National Natural Science Fund number 61802428.
文摘Web Services Choreography Description Language lacks a formal system to accurately express the semantics of service behaviors and verify the correctness of a service choreography model.This paper presents a new approach of choreography model verification based on Description Logic.A meta model of service choreography is built to provide a conceptual framework to capture the formal syntax and semantics of service choreography.Based on the framework,a set of rules and constraints are defined in Description Logic for choreography model verification.To automate model verification,the UML-based service choreography model will be transformed,by the given algorithms,into the DL-based ontology,and thus the model properties can be verified by reasoning through the ontology with the help of a popular DL reasoned.A case study is given to demonstrate applicability of the method.Furthermore,the work will be compared with other related research.
文摘In contemporary times,with the development of multimedia technology,especially in consideration of the advantages of multimedia technology in performance,dance,as an expressive art,is bound to be concatenated with multimedia technology to enrich its form of display.The influence of multimedia technology in dance choreography on dance works and the effect of multimedia technology itself on dance choreography are worth further discussion.There is no doubt that with the application of multimedia technology in the dance field,choreographers have more open and creative ideas.Perhaps,in view of the role of multimedia technology in dance creation,the involvement of various disciplines and different technologies in dance choreography would expand in the future.However,it is necessary to consider the integration of new technologies,especially the negative impact of their improper use on the expression of dance works.Therefore,this study aims to explore the elements and relations between multimedia technology and dance choreography in the new era,seek for methods and rules of multimedia technology in dance creation,pursue its positive significance,and provide certain theoretical reference for the creation of dance works through multimedia technology.
基金This work was partly supported by the National Natural Science Foundation of China (Grant No. 19871096) the Qiu Shi Science and Technology Foundation.
文摘In this paper, we give a short proof for the existence of nontrivial choreography solution to the equal-mass three-body problem, which is discovered by Chenciner and Montgomery recently.
文摘Web service choreography describes global mod- els of service interactions among a set of participants. For an interaction to be executed, the participants must know the required channel（s） used in the interaction, otherwise the ex- ecution will get stuck. Since channels are composed dynami- cally, the initial channel set of each participant is often insuf- ficient to meet the requirements. It is the responsibility of the participants to pass required channels owned （known） by one to others. Since service choreography may involve many par- ticipants and complex channel constraints, it is hard for de- signers to specify channel passing in a choreography exactly as required. We address the problem of checking whether a service choreography lacks channels or has redundant chan- nels, and how to automatically generate channel passing based on interaction flows of the service choreography in the case of channel absence. Concretely, we propose a sim- ple language Chorc, a channel interaction sub-language for modeling the channel passing aspect of service choreography. Based on the formal operational semantics of Chore, the algo- rithms for static checking of service choreography and gen- erating channel passing are also studied, and the complexity results of algorithms are discussed. Moreover, some illus- trated service choreography examples are presented to show how to formalize and analyze service choreography with channel passing in Chorc.
基金The National Natural Science Foundation of China(No.60403027,60773191,70771043)the National High Technology Research and Development Program of China(863 Program)(No.2007AA01Z403)
文摘In order to formally reason and verify web services composition described by web services choreography specification WS-CDL,a typed formal model named typed Abstract WS-CDL（web services choreography description language）for WS-CDL specifications is proposed.In typed Abstract WS-CDL,the syntax of type and session,typing rules and operational semantics are formalized;the collaborations of web services are formally described by sessions;the operational semantics of a session can help to formally reason the execution of the choreography;the typing rules can help to formally check the data type consistency of exchanged information between web services and capture run-time errors due to type mismatches.Particularly,the concepts of type assumption set extension and type assumption set compatibility are proposed,and the merging algorithm of type assumption sets is defined so as to eliminate type assumption conflict.Based on the formal model,typed mapping rules for mapping web services choreography to orchestration is also defined.With the typed mapping rules,orchestration stubs and their type assumption sets can be generated from a given choreography; thus, web services composition can be verified at choreography and orchestration levels,respectively.The model is proved to have properties of type safety,and how the model can help to reason and verify web services composition is illustrated through a case study.
基金Project(51975019)supported by the National Natural Science Foundation of ChinaProject(2019 ZX 04024001)supported by the National Science and Technology Major Project of ChinaProject(Z 201100006720008)supported by the Beijing Science and Technology Plan,China。
文摘Discrete manufacturing workshops are confronted with problems of processing diverse products and strict real time requirements for data service calculation and manufacturing equipment,which makes it difficult to provide real time feedback and compensation.In this study,a high-availability,high-performance,and high-concurrency digital twin reference model was constructed to satisfy a large number of manufacturing requirements.A multiterminal real-time interaction model and information aging classification rules for virtual and physical models were established.Moreover,a multiterminal virtual interaction model was proposed,and a generalized distributed computing service digital twinning system was developed.This digital twin system was considered a machine tool box processing line as an actual case.Consequently,a full closed-loop manufacturing process digital twin platform for physical request service,real-time response,and quality information feedback from iterations,which provides case guidance for subsequent factory digital twin systems,was realized.The proposed system can satisfy the requirements of multidevice big data computing services in modern manufacturing plants,as well as multiplatform,low-latency,and high-fidelity information visualization requirements for managers.Thus,this system is expected to play an important role in information factories.
文摘One of the most intellectually challenging and perhaps rewarding engagements in any creative endeavour, be it written literature or performance, is decrypting the metaphorical construct imbued in such a work, within the confines of the intentions of the writer or performer. Beyond coded speech, dance and choreography are works of art which make use of symbols to communicate man＇s thought, experience, and emotions. These symbols are conveyed basically through movement and they are forms of artistic expression to which all men, across climes, can respond, be it in a live performance or recorded video film. More than ever before, the music video film has taken a great place of prominence in the entertainment circles the world over, and musical choreography has become a major tool, used by singers, musicians, and music producers in these video films to enhance their creative output and make their productions more appealing both for economic and aesthetic purposes. This paper examines the motifs of dance and choreography in two Nigerian music videos, namely, Olori Oko （2006） by a Gospel group called Infinity and Roll It （2007） by a hip-hop group named P. Sqanre. The paper investigates the themes of the music, the concepts of the dances, and the styles of choreography in both works. The paper concludes that though both works belong to different genres, they are each successful in their own rights and have both contributed in elevating the standards in the practice of dance and choreography in Nigerian music video film.
文摘The Dikopelo music practice involves vocal singing and dancing in a patterned choreography without musical instruments in which people from a particular area join together to sing as a choir.The element is practiced by men,women and children but is mostly dominated by the elders who, forming an informal council of advisors,transmit their skills to the younger generation.
文摘As a disruptive technology,the blockchain is continuously finding novel application contexts,bringing new opportunities and radical changes.In this paper,we use blockchain as a communication infrastructure to support multi-party business processes.In particular,through smart contracts specifically generated by the mentioned business process,it is possible to derive a trustable infrastructure enabling the interaction among parties.Moreover,the emergence of different blockchain technologies,satisfying different characteristics,gives the possibility to support the same business process dealing with different non-functional needs.In this paper,we propose a novel engineering methodology supported by a practical framework called Multi-Chain.It permits to derive,using a model-driven strategy,a blockchain-based infrastructure,that can be deployed over a specific blockchain technology(e.g.,Ethereum or Hyperledger Fabric).The objective is to permit the single definition and multiple deployments of the business process,to deliver the same functionalities,but satisfying different nonfunctional needs.In such a way,organisations willing to cooperate can select the multi-party business process and the blockchain technology they would like to use to satisfy their needs.Using Multi-Chain,they will be able to automatically derive from a Business Process Modelling Notation(BPMN)choreography diagram a blockchain infrastructure ready to be used.This overcomes the need to get acquainted with many details of the specific technology.
