3,458 papers · page 164 of 173
We report on GADGET, a new software test generation system that uses combinatorial optimization to obtain condition/decision coverage of C/C++ programs. The GADGET system is fully automatic and supports all C/C++ language constructs. This allows us to generate tests for programs …
The authors present a tool-based approach that examines how example programs reuse a particular library. The approach can facilitate reuse by: (1) guiding the developer towards important library classes of general utility; (2) guiding the developer towards library classes particu…
Software inspection is a valuable technique for detecting defects in the products of software development. One avenue of research within inspection concerns the development of computer support. It is hoped that such support will provide even greater benefits when applying inspect…
Most efforts to automate the formal verification of communicating systems have centred around finite-state systems (FSSs). However, FSSs are incapable of modelling many practical communicating systems, and hence there is interest in a novel class of problems, which we call VIPSs …
An effective means for analyzing and reasoning on software systems is to use formal specifications to simulate their execution. The simulation traces can be used for specification testing and reused, later in the development process, for functional testing of the system. It is wi…
Describes a notation and tool for demonstrating to a third-party certifier that software written in a subset of Ada is safe, and gives some experience of using them on real projects. The thesis underlying the design is that people write adequate code, but that they make design an…
The article shows how to make a transition from the Z formal notation to the Business Object Notation (BON). It is demonstrated that BON has the expressive power of Z, with the additional advantages of object-orientation and a supporting seamless development method. The transitio…
Describes a system that improves testing quality by supporting automatic test data selection, execution and result verification. The system tests poorly-encapsulated Ada units against formal specifications. This task is difficult partly because the unit's interface is not explici…
Discusses tools that aid in the development, assessment and reengineering of language descriptions (i.e. syntactic descriptions of a language). We develop assessment tools that give an indication as to what is wrong with an existing language description, and give hints towards it…
Automated user-interface generation environments have been criticized for their failure to deliver rich and powerful interactive applications. To specify more powerful systems, designers require multiple specialized modeling notations. The model-composition problem is concerned w…
Automatic software instrumentation is usually done at the machine level or is targeted at specific program behavior for use with a particular monitoring application. The paper describes CCI, an automatic software instrumentation tool for ANSI C designed to serve a broad range of …
Structural testing criteria are mandated in many software development standards and guidelines. The process of generating test data to achieve 100% coverage of a given structural coverage metric is labour-intensive and expensive. This paper presents an approach to automate the ge…
Cognitive models of software comprehension are potential sources of theoretical knowledge for tool designers. Although their use in the analysis of existing tools is fairly well established, the literature has shown only limited use of such models for directly developing design i…
Structure is important in large specifications for understanding, testing and managing change. Category theory has been explored as framework for providing this structure, and has been successfully used to compose specifications. This work has typically adopted a "correct-by-cons…
The importance of requirements, which in practice often means natural language requirements, for a successful software project cannot be underestimated. Although requirement analysis has been traditionally reserved to the experience of professionals, there is no reason not to use…
This paper deals with non-functional aspects of software. It presents an approach towards the integration of methods in order to handle properties of numerical programs. We develop a program analysis technique which allows us to formalise, evaluate and check non-functional proper…
We describe a proof plan that characterises a family of proofs corresponding to the synthesis of recursive functional programs. This plan provides a significant degree of automation in the construction of recursive programs from specifications, together with correctness proofs. T…
The effectiveness of software engineering technologies depends very much on the situation in which they are applied. In order to further improve software development practices one needs to explicitly describe and utilise knowledge about application domains of software engineering…
Partial evaluation is an optimization technique traditionally used in compilation. We have adapted this technique to the understanding of scientific application programs during their maintenance, and we have implemented a tool that analyzes Fortran 90 application programs and per…
Proofs in the Nuprl system, an implementation of a constructive type theory, yield "correct-by-construction" programs. In this paper a new methodology is presented for extracting efficient and readable programs from inductive proofs. The resulting extracted programs are in a form…