Feature based design has been regarded as a promising approach for CAD/CAM integration.This paper aims to establish a domain independent representation formalism for feature based design in three aspects: formal re...Feature based design has been regarded as a promising approach for CAD/CAM integration.This paper aims to establish a domain independent representation formalism for feature based design in three aspects: formal representation,design process model and design algorithm.The implementing scheme and formal description of feature taxonomy,feature operator,feature model validation and feature transformation are given in the paper.The feature based design process model suited for either sequencial or concurrent engineering is proposed and its application to product structural design and process plan design is presented. Some general design algorithms for developing feature based design system are also addressed.The proposed scheme provides a formal methodology elementary for feature based design system development and operation in a structural way.展开更多
Benefiting from advances in feature technology for design and manufacture can not be expected before a formal methodology is established. This paper makes attempt to establish a definition formalism of machining featu...Benefiting from advances in feature technology for design and manufacture can not be expected before a formal methodology is established. This paper makes attempt to establish a definition formalism of machining features in design for manufacturability from two aspects: formal definition and manufacturability analysis. Some definitions for machining feature based upon the selection and sequencing of material removal operations for component in accordance with the design geometry are presented and a framework of feature based design for manufacturability is outlined correspondingly. The proposed scheme contributes to several aspects of feature based CAD/CAM integration, especially to encourage potentially a more generic approach to the automation of design.展开更多
Based on the definition of a logic structure feature to relate logically functional requirements to geometric representation independent upon detailed geometric representation, this paper presents an idea of logical s...Based on the definition of a logic structure feature to relate logically functional requirements to geometric representation independent upon detailed geometric representation, this paper presents an idea of logical structure modeling for computer aided conceptual design and makes attempt to establish a representation formalism of logic structure modeling. The definition and representation of logical structure feature are given and an assembly module definition for supporting top down conceptual design is also proposed. The proposed scheme contributes to several aspects of conceptual design research, especially to provide elementarily a formal methodology for computer aided conceptual design system development and operation.展开更多
In order to improve the design and implementation quality of web service compositions,formal methods are used to model them and certain properties are verified.WCFA （web service interface control flow automata）is us...In order to improve the design and implementation quality of web service compositions,formal methods are used to model them and certain properties are verified.WCFA （web service interface control flow automata）is used to model web services,especially the control flow and possible interactions with other web services.A web service composition consists of a set of interacting WCFA.The global behavior of web service compositions is captured by NWA（nested word automata）.A variation of the depth-first search algorithm is used to transform a set of WCFA into an NWA.State formulae and call stacks at each node of NWA are computed by a path-sensitive reachability analysis.Safety properties,call stack inspection properties and pre/post-conditions of service invocations are described by assertions.Then verification of these assertions is carried out by an automated SAT tool.展开更多
Based on the authentication tests and the strand space model, the robust email protocol with perfect forward secrecy is formally analyzed, and the security shortcomings of the protocol is pointed out. Meanwhile, the m...Based on the authentication tests and the strand space model, the robust email protocol with perfect forward secrecy is formally analyzed, and the security shortcomings of the protocol is pointed out. Meanwhile, the man-in-the-middle attack to the protocol is given, where the attacker forges the messages in the receiving phase to cheat the two communication parties and makes them share the wrong session keys with him. Therefore, the protocol is not ensured to provide perfect forward secrecy. In order to overcome the above security shortcomings, an advanced email protocol is proposed, where the corresponding signatures in the receiving phase of the protocol are added to overcome the man-in-the-middle attack and ensure to provide perfect forward secrecy. Finally, the proposed advanced email protocol is formally analyzed with the authentication tests and the strand space model, and it is proved to be secure in authentication of the email sender, the recipient and the server. Therefore, the proposed advanced email protocol can really provide perfect forward secrecy.展开更多
For most current Web Service access control methods, Web Service providers create a series of access control roles based on specified attributes. Only by meeting all the roles can a subject obtain the access to necess...For most current Web Service access control methods, Web Service providers create a series of access control roles based on specified attributes. Only by meeting all the roles can a subject obtain the access to necessary operations and resources. However, because of the dynamic and open traits of Web Services, it is difficult for Web Service providers to work out an access control policy with moderate intensity and to realize a satisfactory balance between protecting the security of resources and maintaining the service reachable rate. To provide a solution to the above problem, this paper proposed a trust compensation access control method based on the Attribute-Based Access Control model. Our main contributions include a formal description of the access control method, a method to calculate the attribute trust degree based on time decay, and the trust compensation value of the attribute trust degree, as well as a new Service Oriented Architecture （SOA） architecture and its procedures based on a detailed trust compensation access control method.展开更多
This paper addresses the issue of checking consistency in information models. A method based on constraint programming is proposed for identifying inconsistency or proving consistency in information models. The system...This paper addresses the issue of checking consistency in information models. A method based on constraint programming is proposed for identifying inconsistency or proving consistency in information models. The system described here checks information models written in the ISO standard information modelling language EXPRESS. EXPRESS is part of the ISO STEP standard used in the manufacturing and process industries. This paper describes the checking procedure, including EXPRESS model formalization, constraint satisfaction problem (CSP) derivation from the formalized model and satisfaction checking of the derived CSPs. This paper shows a new domain in which constraint programming can be exploited as model verification and validation.展开更多
AIM: To investigate whether ANNs and LDA could recognize patients with ABG in a database, containing only clinical and biochemical variables, of a pool of patients with and without ABG, by selecting the most predictiv...AIM: To investigate whether ANNs and LDA could recognize patients with ABG in a database, containing only clinical and biochemical variables, of a pool of patients with and without ABG, by selecting the most predictive variables and by reducing input data to the minimum.METHODS: Data was collected from 350 consecutive outpatients (263 with ABG, 87 with non-atrophic gastritis and/or celiac disease [controls]). Structured questionnaires with 22 items (anagraphic, anamnestic, clinical, and biochemical data) were filled out for each patient. All patients underwent gastroscopy with biopsies. ANNs and LDA were applied to recognize patients with ABG.Experiment 1: random selection on 37 variables, experiment 2: optimization process on 30 variables, experiment 3:input data reduction on 8 variables, experiment 4: use of only clinical input data on 5 variables, and experiment 5:use of only serological variables.RESULTS: In experiment 1, overall accuracies of ANNs and LDA were 96.6% and 94.6%, respectively, for predicting patients with ABG. In experiment 2, ANNs and LDA reached an overall accuracy of 98.8% and 96.8%,respectively. In experiment 3, overall accuracy of ANNs was 98.4%. In experiment 4, overall accuracies of ANNs and LDA were, respectively, 91.3% and 88.6%. In experiment 5, overall accuracies of ANNs and LDA were,respectively, 97.7% and 94.5%.CONCLUSION: This preliminary study suggests that advanced statistical methods, not only ANNs, but also LDA,may contribute to better address bioptic sampling during gastroscopy in a subset of patients in whom ABG may be suspected on the basis of aspecific gastrointestinal symptoms or non-digestive disorders.展开更多
The global view of firewall policy conflict is important for administrators to optimize the policy.It has been lack of appropriate firewall policy global conflict analysis,existing methods focus on local conflict dete...The global view of firewall policy conflict is important for administrators to optimize the policy.It has been lack of appropriate firewall policy global conflict analysis,existing methods focus on local conflict detection.We research the global conflict detection algorithm in this paper.We presented a semantic model that captures more complete classifications of the policy using knowledge concept in rough set.Based on this model,we presented the global conflict formal model,and represent it with OBDD(Ordered Binary Decision Diagram).Then we developed GFPCDA(Global Firewall Policy Conflict Detection Algorithm) algorithm to detect global conflict.In experiment,we evaluated the usability of our semantic model by eliminating the false positives and false negatives caused by incomplete policy semantic model,of a classical algorithm.We compared this algorithm with GFPCDA algorithm.The results show that GFPCDA detects conflicts more precisely and independently,and has better performance.展开更多
Nonlinear modeling of a flexible beam with large deformation was investigated. Absolute nodal cooridnate formulation is employed to describe the motion, and Lagrange equations of motion of a flexible beam are derived ...Nonlinear modeling of a flexible beam with large deformation was investigated. Absolute nodal cooridnate formulation is employed to describe the motion, and Lagrange equations of motion of a flexible beam are derived based on the geometric nonlinear theory. Different from the previous nonlinear formulation with Euler-Bernoulli assumption, the shear strain and transverse normal strain are taken into account. Computational example of a flexible pendulum with a tip mass is given to show the effects of the shear strain and transverse normal strain. The constant total energy verifies the correctness of the present formulation.展开更多
The simplest normal form of resonant double Hopf bifurcation was studied based on Lie operator. The coefficients of the simplest normal forms of resonant double Hopf bifurcation and the nonlinear transformations in te...The simplest normal form of resonant double Hopf bifurcation was studied based on Lie operator. The coefficients of the simplest normal forms of resonant double Hopf bifurcation and the nonlinear transformations in terms of the original system coefficients were given explicitly. The nonlinear transformations were used for reducing the lower- and higher-order normal forms, and the rank of system matrix was used to determine the coefficient of normal form which could be reduced. These make the gained normal form simpler than the traditional one. A general program was compiled with Mathematica. This program can compute the simplest normal form of resonant double Hopf bifurcation and the non-resonant form up to the 7th order.展开更多
文摘Feature based design has been regarded as a promising approach for CAD/CAM integration.This paper aims to establish a domain independent representation formalism for feature based design in three aspects: formal representation,design process model and design algorithm.The implementing scheme and formal description of feature taxonomy,feature operator,feature model validation and feature transformation are given in the paper.The feature based design process model suited for either sequencial or concurrent engineering is proposed and its application to product structural design and process plan design is presented. Some general design algorithms for developing feature based design system are also addressed.The proposed scheme provides a formal methodology elementary for feature based design system development and operation in a structural way.
文摘Benefiting from advances in feature technology for design and manufacture can not be expected before a formal methodology is established. This paper makes attempt to establish a definition formalism of machining features in design for manufacturability from two aspects: formal definition and manufacturability analysis. Some definitions for machining feature based upon the selection and sequencing of material removal operations for component in accordance with the design geometry are presented and a framework of feature based design for manufacturability is outlined correspondingly. The proposed scheme contributes to several aspects of feature based CAD/CAM integration, especially to encourage potentially a more generic approach to the automation of design.
文摘Based on the definition of a logic structure feature to relate logically functional requirements to geometric representation independent upon detailed geometric representation, this paper presents an idea of logical structure modeling for computer aided conceptual design and makes attempt to establish a representation formalism of logic structure modeling. The definition and representation of logical structure feature are given and an assembly module definition for supporting top down conceptual design is also proposed. The proposed scheme contributes to several aspects of conceptual design research, especially to provide elementarily a formal methodology for computer aided conceptual design system development and operation.
基金The National Key Technology R&D Program of Chinaduring the 11th Five-Year Plan Period(No.2006BAH02A12)the National High Technology Research and Development Program of China(863 Program)(No.2006AA010101)
文摘In order to improve the design and implementation quality of web service compositions,formal methods are used to model them and certain properties are verified.WCFA （web service interface control flow automata）is used to model web services,especially the control flow and possible interactions with other web services.A web service composition consists of a set of interacting WCFA.The global behavior of web service compositions is captured by NWA（nested word automata）.A variation of the depth-first search algorithm is used to transform a set of WCFA into an NWA.State formulae and call stacks at each node of NWA are computed by a path-sensitive reachability analysis.Safety properties,call stack inspection properties and pre/post-conditions of service invocations are described by assertions.Then verification of these assertions is carried out by an automated SAT tool.
基金The Natural Science Foundation of Jiangsu Province(No.BK2006108)
文摘Based on the authentication tests and the strand space model, the robust email protocol with perfect forward secrecy is formally analyzed, and the security shortcomings of the protocol is pointed out. Meanwhile, the man-in-the-middle attack to the protocol is given, where the attacker forges the messages in the receiving phase to cheat the two communication parties and makes them share the wrong session keys with him. Therefore, the protocol is not ensured to provide perfect forward secrecy. In order to overcome the above security shortcomings, an advanced email protocol is proposed, where the corresponding signatures in the receiving phase of the protocol are added to overcome the man-in-the-middle attack and ensure to provide perfect forward secrecy. Finally, the proposed advanced email protocol is formally analyzed with the authentication tests and the strand space model, and it is proved to be secure in authentication of the email sender, the recipient and the server. Therefore, the proposed advanced email protocol can really provide perfect forward secrecy.
文摘For most current Web Service access control methods, Web Service providers create a series of access control roles based on specified attributes. Only by meeting all the roles can a subject obtain the access to necessary operations and resources. However, because of the dynamic and open traits of Web Services, it is difficult for Web Service providers to work out an access control policy with moderate intensity and to realize a satisfactory balance between protecting the security of resources and maintaining the service reachable rate. To provide a solution to the above problem, this paper proposed a trust compensation access control method based on the Attribute-Based Access Control model. Our main contributions include a formal description of the access control method, a method to calculate the attribute trust degree based on time decay, and the trust compensation value of the attribute trust degree, as well as a new Service Oriented Architecture （SOA） architecture and its procedures based on a detailed trust compensation access control method.
文摘This paper addresses the issue of checking consistency in information models. A method based on constraint programming is proposed for identifying inconsistency or proving consistency in information models. The system described here checks information models written in the ISO standard information modelling language EXPRESS. EXPRESS is part of the ISO STEP standard used in the manufacturing and process industries. This paper describes the checking procedure, including EXPRESS model formalization, constraint satisfaction problem (CSP) derivation from the formalized model and satisfaction checking of the derived CSPs. This paper shows a new domain in which constraint programming can be exploited as model verification and validation.
基金Supported by a grant from Bracco Imaging Spa, Milan, Italy, and a grant from the Italian Ministry of University and Research (No. 2002-2003)
文摘AIM: To investigate whether ANNs and LDA could recognize patients with ABG in a database, containing only clinical and biochemical variables, of a pool of patients with and without ABG, by selecting the most predictive variables and by reducing input data to the minimum.METHODS: Data was collected from 350 consecutive outpatients (263 with ABG, 87 with non-atrophic gastritis and/or celiac disease [controls]). Structured questionnaires with 22 items (anagraphic, anamnestic, clinical, and biochemical data) were filled out for each patient. All patients underwent gastroscopy with biopsies. ANNs and LDA were applied to recognize patients with ABG.Experiment 1: random selection on 37 variables, experiment 2: optimization process on 30 variables, experiment 3:input data reduction on 8 variables, experiment 4: use of only clinical input data on 5 variables, and experiment 5:use of only serological variables.RESULTS: In experiment 1, overall accuracies of ANNs and LDA were 96.6% and 94.6%, respectively, for predicting patients with ABG. In experiment 2, ANNs and LDA reached an overall accuracy of 98.8% and 96.8%,respectively. In experiment 3, overall accuracy of ANNs was 98.4%. In experiment 4, overall accuracies of ANNs and LDA were, respectively, 91.3% and 88.6%. In experiment 5, overall accuracies of ANNs and LDA were,respectively, 97.7% and 94.5%.CONCLUSION: This preliminary study suggests that advanced statistical methods, not only ANNs, but also LDA,may contribute to better address bioptic sampling during gastroscopy in a subset of patients in whom ABG may be suspected on the basis of aspecific gastrointestinal symptoms or non-digestive disorders.
基金supported by the National Nature Science Foundation of China under Grant No.61170295 the Project of National ministry under Grant No.A2120110006+2 种基金 the Co-Funding Project of Beijing Municipal Education Commission under Grant No.JD100060630 the Beijing Education Committee General Program under Grant No. KM201211232010 the National Nature Science Foundation of China under Grant NO. 61370065
文摘The global view of firewall policy conflict is important for administrators to optimize the policy.It has been lack of appropriate firewall policy global conflict analysis,existing methods focus on local conflict detection.We research the global conflict detection algorithm in this paper.We presented a semantic model that captures more complete classifications of the policy using knowledge concept in rough set.Based on this model,we presented the global conflict formal model,and represent it with OBDD(Ordered Binary Decision Diagram).Then we developed GFPCDA(Global Firewall Policy Conflict Detection Algorithm) algorithm to detect global conflict.In experiment,we evaluated the usability of our semantic model by eliminating the false positives and false negatives caused by incomplete policy semantic model,of a classical algorithm.We compared this algorithm with GFPCDA algorithm.The results show that GFPCDA detects conflicts more precisely and independently,and has better performance.
基金National Natural Science Foundation ofChina (No.10472066,10372057)
文摘Nonlinear modeling of a flexible beam with large deformation was investigated. Absolute nodal cooridnate formulation is employed to describe the motion, and Lagrange equations of motion of a flexible beam are derived based on the geometric nonlinear theory. Different from the previous nonlinear formulation with Euler-Bernoulli assumption, the shear strain and transverse normal strain are taken into account. Computational example of a flexible pendulum with a tip mass is given to show the effects of the shear strain and transverse normal strain. The constant total energy verifies the correctness of the present formulation.
基金Supported by National Natural Science Foundation of China(No. 10372068).
文摘The simplest normal form of resonant double Hopf bifurcation was studied based on Lie operator. The coefficients of the simplest normal forms of resonant double Hopf bifurcation and the nonlinear transformations in terms of the original system coefficients were given explicitly. The nonlinear transformations were used for reducing the lower- and higher-order normal forms, and the rank of system matrix was used to determine the coefficient of normal form which could be reduced. These make the gained normal form simpler than the traditional one. A general program was compiled with Mathematica. This program can compute the simplest normal form of resonant double Hopf bifurcation and the non-resonant form up to the 7th order.
