Model checking techniques have been widely used in verifying web service compositions to ensure the trustworthi- ness. However, little research has focused on testing web services. Based on the research of model check...Model checking techniques have been widely used in verifying web service compositions to ensure the trustworthi- ness. However, little research has focused on testing web services. Based on the research of model checking techniques~ we propose a model checking based approach for testing web service composition which is described by using the web services choreography description language （WS-CDL）. According to worldwide web consortium （W3C） candidate recommendation, the WS-CDL specification provides a language for characterizing interactions between distinct web services using XML. Since the behaviors of web service composition are asynchronous, distributed, low-coupled and platform independent, we employ the guarded automata （GA） model for specifying the composition described in WS-CDL and using the simple promela interpreter （SPIN） model checker for detecting the collaborations of web services. Test cases can be transformed from counterexamples generated by SPIN using adequacy criteria. In this paper we apply the transition coverage criterion for generating counterex- amples. To illustrate our approach, we set ＂E-commerce service system＂ as an example for demonstrating how test cases can be generated using SPIN for compositions specified in WS-CDL.展开更多
Lustre is a formal synchronous declarative language widely used for modeling and specifying safety critical applications in the fields of avionics, transportation, and energy production. In such applications, the test...Lustre is a formal synchronous declarative language widely used for modeling and specifying safety critical applications in the fields of avionics, transportation, and energy production. In such applications, the testing activity to ensure correctness of the system plays a crucial role. During the development process, Lustre programs (or SCADE) are often upgraded, so regression test should be performed to detect bugs. However, regression test is generally costly, because the number of test cases is usually very large. In this paper, we present the solution to automatically generating test cases in regression testing of Lustre/SCADE programs. We apply this solution to regression testing for case study Uturn System.展开更多
The mechanical behaviour of a quasi-brittle material,i.e.Pietra Serena sandstone,was investigated both numerically and experimentally in order to build a reliable numerical modelling system applicable to more complex ...The mechanical behaviour of a quasi-brittle material,i.e.Pietra Serena sandstone,was investigated both numerically and experimentally in order to build a reliable numerical modelling system applicable to more complex cases.The Karagozian and Case concrete(KCC)model was exploited as the material constitutive law and a new method to utilise this model for efficient and accurate simulation of quasibrittle materials is discussed.The capability of this model is evaluated by comparing the results of the numerical simulations with the corresponding experimental results,and the method itself is critically assessed.展开更多
In software industry the major problem encountered during project scheduling is in deciding what proportion of the resources has allocated to the testing phase. In general it has been observed that about 40%-50% of th...In software industry the major problem encountered during project scheduling is in deciding what proportion of the resources has allocated to the testing phase. In general it has been observed that about 40%-50% of the resources need to be allocated to the testing phase. However it is very difficult to predict the exact amount of effort required to be allocated to testing phase. As a result the project planning goes haywire. The project which has not been tested sufficiently can cause huge losses to the organization. This research paper focuses on finding a method which gives a measure of the effort to be spent on the testing phase. This paper provides effort estimates during pre-coding and post-coding phases using neural network to predict more accurately.展开更多
Objectives: Developing inference procedures on the quasi-binomial distribution and the regression model. Methods: Score testing and the method of maximum likelihood for regression parameters estimation. Data: Several ...Objectives: Developing inference procedures on the quasi-binomial distribution and the regression model. Methods: Score testing and the method of maximum likelihood for regression parameters estimation. Data: Several examples are included, based on published data. Results: A quasi-binomial model is used to model binary response data which exhibit extra-binomial variation. A partial score test on the binomial hypothesis versus the quasi-binomial alternative is developed and illustrated on three data sets. The extended logit transformation on the binomial parameter is introduced and the large sample dispersion matrix of the estimated parameters is derived. The Nonlinear Mixed Procedure (NLMIXED) in SAS is shown to be very appropriate for the estimation of nonlinear regression.展开更多
Debugging software code has been a challenge for software developers since the early days of computer programming. A simple need, because the world is run by software. So perhaps the biggest engineering challenge is f...Debugging software code has been a challenge for software developers since the early days of computer programming. A simple need, because the world is run by software. So perhaps the biggest engineering challenge is finding ways to make software more reliable. This review provides an overview of techniques developed over time in the field of software model checking to solve the problem of detecting errors in program code. In addition, the challenges posed by this technology are discussed and ways to mitigate them in future research and applications are proposed. A comprehensive examination of the various model verification methods used to detect program code errors is intended to lay the foundation for future research in this area.展开更多
为改善传统的模糊测试用例生成方法存在指令覆盖率低和效率不足的问题,提出一种大语言模型(Large Language Model,LLM)辅助智能合约模糊测试用例生成方法IntelliFuzz。该方法通过静态分析提取目标智能合约的潜在漏洞信息,并构建初始状...为改善传统的模糊测试用例生成方法存在指令覆盖率低和效率不足的问题,提出一种大语言模型(Large Language Model,LLM)辅助智能合约模糊测试用例生成方法IntelliFuzz。该方法通过静态分析提取目标智能合约的潜在漏洞信息,并构建初始状态交易对语料库和婴态语料库,从状态交易对语料库中选取状态交易对进行变异并执行,同时监测路径点覆盖率变化,将有效提升覆盖率的样本补充至状态交易对语料库。当覆盖率达到瓶颈时,调用思维链提示工程模块生成当前状态下新的交易序列,若评估结果能提高指令覆盖率,则将新生成的交易序列保存到状态和交易对语料库中。实验结果表明,与基准方法ItyFuzz相比,IntelliFuzz在小型合约10 s内的指令覆盖率提升11%,在大型合约20 s内的指令覆盖率提升40.9%,且IntelliFuzz在B2数据集误报率降低9.4%,漏报率降低3.98%,模糊测试用例生成的指令覆盖率和效率有所提升。展开更多
基金Project supported by the Open Foundation of State Key Laboratory of Software Engineering(Grant No.SKLSE20080712)the National Natural Science Foundation of China(Grant No.60970007)+2 种基金the National Basic Research Program of China(Grant No.2007CB310800)the Shanghai Leading Academic Discipline Project(Grant No.J50103)the Science and Technology Commission of Shanghai Municipality(Grant No.09DZ2272600)
文摘Model checking techniques have been widely used in verifying web service compositions to ensure the trustworthi- ness. However, little research has focused on testing web services. Based on the research of model checking techniques~ we propose a model checking based approach for testing web service composition which is described by using the web services choreography description language （WS-CDL）. According to worldwide web consortium （W3C） candidate recommendation, the WS-CDL specification provides a language for characterizing interactions between distinct web services using XML. Since the behaviors of web service composition are asynchronous, distributed, low-coupled and platform independent, we employ the guarded automata （GA） model for specifying the composition described in WS-CDL and using the simple promela interpreter （SPIN） model checker for detecting the collaborations of web services. Test cases can be transformed from counterexamples generated by SPIN using adequacy criteria. In this paper we apply the transition coverage criterion for generating counterex- amples. To illustrate our approach, we set ＂E-commerce service system＂ as an example for demonstrating how test cases can be generated using SPIN for compositions specified in WS-CDL.
文摘Lustre is a formal synchronous declarative language widely used for modeling and specifying safety critical applications in the fields of avionics, transportation, and energy production. In such applications, the testing activity to ensure correctness of the system plays a crucial role. During the development process, Lustre programs (or SCADE) are often upgraded, so regression test should be performed to detect bugs. However, regression test is generally costly, because the number of test cases is usually very large. In this paper, we present the solution to automatically generating test cases in regression testing of Lustre/SCADE programs. We apply this solution to regression testing for case study Uturn System.
文摘The mechanical behaviour of a quasi-brittle material,i.e.Pietra Serena sandstone,was investigated both numerically and experimentally in order to build a reliable numerical modelling system applicable to more complex cases.The Karagozian and Case concrete(KCC)model was exploited as the material constitutive law and a new method to utilise this model for efficient and accurate simulation of quasibrittle materials is discussed.The capability of this model is evaluated by comparing the results of the numerical simulations with the corresponding experimental results,and the method itself is critically assessed.
文摘In software industry the major problem encountered during project scheduling is in deciding what proportion of the resources has allocated to the testing phase. In general it has been observed that about 40%-50% of the resources need to be allocated to the testing phase. However it is very difficult to predict the exact amount of effort required to be allocated to testing phase. As a result the project planning goes haywire. The project which has not been tested sufficiently can cause huge losses to the organization. This research paper focuses on finding a method which gives a measure of the effort to be spent on the testing phase. This paper provides effort estimates during pre-coding and post-coding phases using neural network to predict more accurately.
文摘Objectives: Developing inference procedures on the quasi-binomial distribution and the regression model. Methods: Score testing and the method of maximum likelihood for regression parameters estimation. Data: Several examples are included, based on published data. Results: A quasi-binomial model is used to model binary response data which exhibit extra-binomial variation. A partial score test on the binomial hypothesis versus the quasi-binomial alternative is developed and illustrated on three data sets. The extended logit transformation on the binomial parameter is introduced and the large sample dispersion matrix of the estimated parameters is derived. The Nonlinear Mixed Procedure (NLMIXED) in SAS is shown to be very appropriate for the estimation of nonlinear regression.
文摘Debugging software code has been a challenge for software developers since the early days of computer programming. A simple need, because the world is run by software. So perhaps the biggest engineering challenge is finding ways to make software more reliable. This review provides an overview of techniques developed over time in the field of software model checking to solve the problem of detecting errors in program code. In addition, the challenges posed by this technology are discussed and ways to mitigate them in future research and applications are proposed. A comprehensive examination of the various model verification methods used to detect program code errors is intended to lay the foundation for future research in this area.
文摘为改善传统的模糊测试用例生成方法存在指令覆盖率低和效率不足的问题,提出一种大语言模型(Large Language Model,LLM)辅助智能合约模糊测试用例生成方法IntelliFuzz。该方法通过静态分析提取目标智能合约的潜在漏洞信息,并构建初始状态交易对语料库和婴态语料库,从状态交易对语料库中选取状态交易对进行变异并执行,同时监测路径点覆盖率变化,将有效提升覆盖率的样本补充至状态交易对语料库。当覆盖率达到瓶颈时,调用思维链提示工程模块生成当前状态下新的交易序列,若评估结果能提高指令覆盖率,则将新生成的交易序列保存到状态和交易对语料库中。实验结果表明,与基准方法ItyFuzz相比,IntelliFuzz在小型合约10 s内的指令覆盖率提升11%,在大型合约20 s内的指令覆盖率提升40.9%,且IntelliFuzz在B2数据集误报率降低9.4%,漏报率降低3.98%,模糊测试用例生成的指令覆盖率和效率有所提升。
