Through reusing software test components, automated software testing generally costs less than manual software testing. There has been much research on how to develop the reusable test components, but few fall on how ...Through reusing software test components, automated software testing generally costs less than manual software testing. There has been much research on how to develop the reusable test components, but few fall on how to estimate the reusability of test conlponents for automated testing. The purpose of this paper is to present a method of minimum reusability estimation for automated testing based on the return on investment （ROI） model. Minimum reusability is a benchmark for the whole automated testing process. If the reusability in one test execution is less than the minimum reusability, some new strategies must be adopted ill the next test execution to increase the reusability. Only by this way, we can reduce unnecessary costs and finally get a return on the investment of automated testing.展开更多
Technologies such as Advanced Driving Assistance System(ADAS)and Vehicle-to-Everything(V2X)in Connected and Automated Vehicles(CAVs)have greatly enhanced the comfort and convenience of driving.However,the increasing l...Technologies such as Advanced Driving Assistance System(ADAS)and Vehicle-to-Everything(V2X)in Connected and Automated Vehicles(CAVs)have greatly enhanced the comfort and convenience of driving.However,the increasing levels of intelligence and connectivity also expose CAVs to severe cybersecurity risks.The vehicles,Internet of Vehicles(IoV)and the cloud servers for CAVs are vulnerable to cyberattacks.Furthermore,many standards and regulations require Original Equipment Manufacturers(OEMs)to consider potential cybersecurity threats when designing and developing CAV products.Consequently,ensuring the cybersecurity for vehicles,networks,and the cloud has become a critical issue that OEMs must address.However,the vast number of CAVs and the variety of the vehicular network make it difficult for the existing cybersecurity assessment and protection methods to satisfy the requirements of the entire vehicle,IoV and cloud.This paper reviews the cybersecurity requirements and potential vulnerabilities of CAVs,the IoV,and cloud servers.Existing cybersecurity assessment,protection and operation methods are summarized.A novel resilient cybersecurity management system is proposed to address the cybersecurity challenges of CAVs.This proposed system can orchestrate management policies and allocate resources based on the urgency of cybersecurity tasks across the vehicle,IoV and cloud,which is suitable for the rapidly evolving CAVs and the continuously expanding services.展开更多
A method using quantifier-elimination is proposed for automatically generating program invariants/inductive assertions. Given a program, inductive assertions, hypothesized as parameterized formulas in a theory, are as...A method using quantifier-elimination is proposed for automatically generating program invariants/inductive assertions. Given a program, inductive assertions, hypothesized as parameterized formulas in a theory, are associated with program locations. Parameters in inductive assertions are discovered by generating constraints on parameters by ensuring that an inductive assertion is indeed preserved by all execution paths leading to the associated location of the program. The method can be used to discover loop invariants-properties of variables that remain invariant at the entry of a loop. The parameterized formula can be successively refined by considering execution paths one by one; heuristics can be developed for determining the order in which the paths are considered. Initialization of program variables as well as the precondition and postcondition, if available, can also be used to further refine the hypothesized invariant. The method does not depend on the availability of the precondition and postcondition of a program. Constraints on parameters generated in this way are solved for possible values of parameters. If no solution is possible, this means that an invariant of the hypothesized form is not likely to exist for the loop under the assumptions/approximations made to generate the associated verification condition. Otherwise, if the parametric constraints are solvable, then under certain conditions on methods for generating these constraints, the strongest possible invariant of the hypothesized form can be generated from most general solutions of the parametric constraints. The approach is illustrated using the logical languages of conjunction of polynomial equations as well as Presburger arithmetic for expressing assertions.展开更多
FGSPEC is a wide spectrum specification language intended to facilitate the software specification and the expression of transformation process from the functional specification which describes“what to do”to the cor...FGSPEC is a wide spectrum specification language intended to facilitate the software specification and the expression of transformation process from the functional specification which describes“what to do”to the corresponding design(operational)specification which describes“how to do”.The design emphasizes the coherence of multi-level specification mechanisms and a tree structure model is provided which unifies the wide spectrum specification styles from“what”to“how”.展开更多
基金Foundation item： the National Natural Science Foundation of China （No. 90718037）
文摘Through reusing software test components, automated software testing generally costs less than manual software testing. There has been much research on how to develop the reusable test components, but few fall on how to estimate the reusability of test conlponents for automated testing. The purpose of this paper is to present a method of minimum reusability estimation for automated testing based on the return on investment （ROI） model. Minimum reusability is a benchmark for the whole automated testing process. If the reusability in one test execution is less than the minimum reusability, some new strategies must be adopted ill the next test execution to increase the reusability. Only by this way, we can reduce unnecessary costs and finally get a return on the investment of automated testing.
基金supported in part by the National Key Research and Development Program of China under Grant Number 2022YFB3104900the National Natural Science Foundation of China(U22A2042).
文摘Technologies such as Advanced Driving Assistance System(ADAS)and Vehicle-to-Everything(V2X)in Connected and Automated Vehicles(CAVs)have greatly enhanced the comfort and convenience of driving.However,the increasing levels of intelligence and connectivity also expose CAVs to severe cybersecurity risks.The vehicles,Internet of Vehicles(IoV)and the cloud servers for CAVs are vulnerable to cyberattacks.Furthermore,many standards and regulations require Original Equipment Manufacturers(OEMs)to consider potential cybersecurity threats when designing and developing CAV products.Consequently,ensuring the cybersecurity for vehicles,networks,and the cloud has become a critical issue that OEMs must address.However,the vast number of CAVs and the variety of the vehicular network make it difficult for the existing cybersecurity assessment and protection methods to satisfy the requirements of the entire vehicle,IoV and cloud.This paper reviews the cybersecurity requirements and potential vulnerabilities of CAVs,the IoV,and cloud servers.Existing cybersecurity assessment,protection and operation methods are summarized.A novel resilient cybersecurity management system is proposed to address the cybersecurity challenges of CAVs.This proposed system can orchestrate management policies and allocate resources based on the urgency of cybersecurity tasks across the vehicle,IoV and cloud,which is suitable for the rapidly evolving CAVs and the continuously expanding services.
基金This research was partially supported by an National Science Foundation(NSF)Information Technology Research(ITR)award CCR-0113611an NSF award CCR-0203051.
文摘A method using quantifier-elimination is proposed for automatically generating program invariants/inductive assertions. Given a program, inductive assertions, hypothesized as parameterized formulas in a theory, are associated with program locations. Parameters in inductive assertions are discovered by generating constraints on parameters by ensuring that an inductive assertion is indeed preserved by all execution paths leading to the associated location of the program. The method can be used to discover loop invariants-properties of variables that remain invariant at the entry of a loop. The parameterized formula can be successively refined by considering execution paths one by one; heuristics can be developed for determining the order in which the paths are considered. Initialization of program variables as well as the precondition and postcondition, if available, can also be used to further refine the hypothesized invariant. The method does not depend on the availability of the precondition and postcondition of a program. Constraints on parameters generated in this way are solved for possible values of parameters. If no solution is possible, this means that an invariant of the hypothesized form is not likely to exist for the loop under the assumptions/approximations made to generate the associated verification condition. Otherwise, if the parametric constraints are solvable, then under certain conditions on methods for generating these constraints, the strongest possible invariant of the hypothesized form can be generated from most general solutions of the parametric constraints. The approach is illustrated using the logical languages of conjunction of polynomial equations as well as Presburger arithmetic for expressing assertions.
文摘FGSPEC is a wide spectrum specification language intended to facilitate the software specification and the expression of transformation process from the functional specification which describes“what to do”to the corresponding design(operational)specification which describes“how to do”.The design emphasizes the coherence of multi-level specification mechanisms and a tree structure model is provided which unifies the wide spectrum specification styles from“what”to“how”.
