Browsing by Author "He, Xudong"
Now showing 1 - 4 of 4
Results Per Page
Sort Options
- A Comparison of Formal Definitions of ADA TaskingHe, Xudong; Lee, John A. N. (Department of Computer Science, Virginia Polytechnic Institute & State University, 1989)In this paper, various formalisms (the operational approach, the denotational approach, the axiomatic approach, Petri nets and temporal logic) are briefly introduced through their applications in formally defining Ada tasking, and their coverages and relative merits are then
- Coverage Analysis Methods for Formal Software TestingLee, John A. N.; He, Xudong (Department of Computer Science, Virginia Polytechnic Institute & State University, 1987)Software creation requires not only testing during the development cycle by the development staff, but also independent validation following the completion of the implementation. However in the latter case, the amount of testing that can be carried out is often limited by time and resources. At the very most, independent testing can be expected to provide 100% coverage of the requirements (or specifications) associated with the software element. This report describes a methodology by which the amount of testing required to provide 100% coverage of the requirements is assured while at the same time minimizing the total number of tests included in a test suite. A collateral procedure provides recommendations on which tests which might be eliminated if less than 10O% coverage of the requirements is permitted. This latter process will be useful in determining the risk of not running the minimum set of tests for 100% coverage. A second process selects from the test matrix the set of tests to be applied to the system following maintenance modification of any module-- that is, to provide a submatrix for regression testing.
- Integrating formal specification and verification methods in software developmentHe, Xudong (Virginia Polytechnic Institute and State University, 1989)This dissertation is a part of an intended long-term research project with the objectives to make software development more scientific and rigorous, thereby to achieve better software quality and to facilitate automated software production; and has two major components: the design of the specification transition paradigm for software development and the theoretical study of the system specification phase in the paradigm. First, after an extensive analysis and comparison of various formalisms, a paradigm for integrating various formal specification and verification methods (predicate transition Petri nets, first order temporal logic, the algebraic, the axiomatic, the denotational, and the operational approaches) in software development has been developed. The model more effectively incorporates foremost formalisms than any other models (the Automatic Programming Project [Bal85], the CIP Project [ClP85], the Larch Project [GHW85] and the RAISE Project [MG87]) and has the following distinctive features: (1) specifications are viewed both as a set of products and a set of well-defined steps of a process, (2) specifications (as a set of products) at different development steps are to be written and verified by different formalisms, (3) specification (as a process) spans from the requirement phase to the detailed design phase, (4) specification for both concurrent and sequential software is supported, and (5) specifications for different aspects (concurrent control abstraction, data abstraction, and procedural abstraction) of a piece of software are dealt with separately. Second, an intensive and in-depth investigation of the system specification phase in the paradigm results in: - a design methodology for predicate transition nets, which incorporates the separate definition technique in Ada [Ada83] and state decomposition technique in Statechart [Har88] into the traditional transformation techniques for Petri nets, and therefore will significantly reduce the design complexity and enhance the comprehensibility of large predicate transition net specifications; - the establishment of a fundamental relationship between predicate transition nets and first order temporal logic and the design of an algorithm for systematically translating predicate transition nets into equivalent temporal logic formulae. Therefore the goal to combine the strengths of both formalisms, i.e. to use predicate transition nets as a specification method and to use temporal logic as a verification method, is achieved; and - the discovery of a special temporal logic proof technique based on a Hilbert-style logic system to verify various properties of predicate transition nets and the associated theorems. Thus temporal logic is effectively used as an analysis method for both safety and liveness properties of predicate transition nets.
- A Methodology for Test SelectionLee, John A. N.; He, Xudong (Department of Computer Science, Virginia Polytechnic Institute & State University, 1988)Software creation requires not only testing during the development cycle by the development staff, but also independent testing following the completion of the implementation. However in the latter case, the amount of testing that can be carried out is often limited by time and resources. At the very most, independent testing can be expected to provide 100% test coverage of the test requirements (or specifications) associated with the software element with the minimum of effort. This paper describes a methodology employing integer programming by which the amount of testing required to provide the maximum possible test coverage of the test requirements (for the given test set) is assured while at the same time minimizing the total number of tests to be included in a test suite. A collateral procedure provides recommendations on which tests might be eliminated if less than 100% test coverage of the test requirements is permitted. This latter procedure will be useful in determining the risk of not running the minimum set of tests for 100% test coverage. A third process selects from the test matrix the set of tests to be applied to the system following maintenance modification of any test requirements-- that is, to provide a submatrix for regression testing. The potential benefits for applying the integer programming technique in test data selection is also discussed.