12212241
Java Implementation Verification Using Reverse Engineering
An approach to system verification is described in which design artefacts produced during forward engineering are automatically compared to corresponding artefacts produced during reverse engineering. The goal is to automatically determine if an implementation is consistent with the original design. In the system described, XML Metadata Interchange (XMI) representations of Unified Modelling Language (UML) class diagrams are recovered from compiled Java class files. These are automatically compared with the corresponding diagrams produced during forward engineering by software engineers using CASE tools. Examples are provided in which reversed engineered UML class diagrams differ from those produced during forward engineering but are still faithful to the original design intent. Such differences are often due to more abstract system representations being captured in forward engineered design artefacts, the inclusion of design attributes and annotations that are not retained in the final implementation, and issues associated with the use of weakly typed containers. In other cases, differences indicate a deviation from the intended design. It is this latter type of difference that this paper is particularly interested in identifying. We advocate that an automated comparison of forward and reverse engineering artefacts should be performed during formal code inspection preparation and used to guide human review of the identified differences.
583415
Using dependence graphs to assist manual and automated object oriented software inspections
Many researchers have demonstrated the value of software inspections in finding and fixing defects early in the development process. However, manual inspection can be a labour-intensive process. We present a tool that applies dependence graphs to aid object oriented software inspection. Our tool, Coffee Grinder, uses control and data dependence graphs both to immediately visualise a Java system and to facilitate the development of scripts to find defects or locate areas of potential inspection interest. These scripts can output results textually or graphically. We present the design of Coffee Grinder and several example scripts. Coffee Grinder illustrates the case for extensible tool support in the software inspection process
60884961
The benefit of information technology in managing outcomes focused curriculum development across related degree programs
This paper describes an interactive, web-based tool that provides access to an Outcomes Database for managing an Outcomes Focused curriculum plan. The approach provides a rapid way to involve subject specialists, course controllers, curriculum designers and educational consultants in the curriculum design and review process. The Outcomes Database is used to capture the relationships between units (i.e. subjects), Unit Learning Outcomes, Course Learning Outcomes, Generic Graduate Attributes and assessments. This is undertaken across courses (i.e. undergraduate degree programs) sharing common units in Information Technology, Computer Science, and Software Engineering. Automatically generated database reports that show how units contribute to the development of the generic graduate attributes are compared to those derived manually on a unit-by-unit basis. Preliminary experience with this IT-based approach demonstrates that automatically generated database reports effectively highlight areas requiring further attention during subsequent curriculum development iterations. The tools and approach described here show how the Outcomes Database can assist in making the transition from an existing program to one using an Outcomes Focused approach.
6716103
Reading the fine print: what benchmarks don't tell you
computer is the most general tool ever developed by mankind. Computers differ from other tools, like cars, in that they can be used in an almost limitless ways. A car has little purpose other than to efficiently move people and things short distances over smooth terrain. A graphics computer, on the other hand, might be used for a wide variety of complex applications including industrial package design, battle simulation, earth resource analysis, medical diagnosis and surgical planning, genetic research, or virtual reality games. During the early days of the auto industry, there was little need to provide information to help customers decide which car to buy. Nowadays, manufacturers provide all sorts of specifications to help people make purchasing decisions, including engine size, miles per gallon, time to accelerate from 0 to 50, trunk size, and so on. When combined with the price and the appearance of the car, these specifications and performance metrics can help consumers decide which of the many makes and models of car to buy. We are in the Model-T stage of developing specifications and performance metrics that help people make computer purchasing decisions. It is clear that the performance of a graphics computer has a large bearing on its ability to solve complex problems, but the problems themselves are of such a wide variety that it is extremely difficult to characterize the machine's performance for all the uses to which it might be put. We have some extremely crude ways to characterize the performance of the pieces that make up a graphics computer. But we have not yet succeeded in developing performance metrics that enable people to easily see whether a graphics computer will have sufficient performance for the problem set that is important to them. A great deal of energy has been invested in developing ways to quantify graphics performance. Have these efforts helped the industry or have they only served to confuse people even more? This panel takes a look at the attempts that have been made to develop useful measures of graphics performance and how those measurements may be used to compare systems from different vendors. More importantly, the panelists will describe the cave-ats and limitations of various benchmarking metrics and provide some real-world insight into how people might be able to apply published graphics benchmark results to their own needs. Background As a precursor to NCGA's Graphics Performance Characterization (GPC) Committee, the …
9257101
More Powerful Z Data Refinement: Pushing the State of the Art in Industrial Refinement
We have recently completed the specification and full refinement proof of a large, industrial scale application. The application was security critical, and the modelling and proof was done to increase the client’s assurance that the implemented system had no design flaws with security implications. Here we describe the application, and then discuss an essential lesson to learn concerning large proof contracts: that one must forge a path between mathematical formality on the one hand and practical achievement of results on the other. We present a number of examples of such decision points, explaining the considerations that must be made in each case.
2090341
Z in practice
Using Z. Structure, Process, Fluency. The Established Strategy. Security Properties. Other Approaches to Z Specification. Validation. Putting Together Your Method. House Style. A Word Counting Utility. Roles in Space. Structuring a Video Shop. Promoting Snakes and Ladders. Refining the Tower of Hanoi. Be Abstract. Sets or Functions?. Sets, Quantifiers, or Toolkit?. Sequences are Functions are Relations are Sets. Error Handling Styles. Promotion. Using Free Types. Using Bags. A Function Calculator. Making Schemas Work for you. Exploiting the Power of the Language. A Real Number Toolkit. and Finally...
10533628
Formal Methods for Industrial Products
We have recently completed the specification and security proof of a large, industrial scale application. The application is security critical, and the modelling and proof were done to increase the client's assurance that the implemented system had no design flaws with security implications. Here we describe the application, specification structure, and proof approach. 
 
One of the security properties of our system is of the kind not preserved in general by refinement. We had to perform a proof that this property, expressed over traces, holds in our state-and-operations style model.
20544062
The Use of Z
During 1990 and 1991 we carried out a survey of Z users in the UK; in this paper we present the results. Z is being used by a wide variety of companies for many different applications. Many institutions use Z because they choose to, rather than because it is mandated by a defence or security related client. Half of the participants in the survey were first- time users of Z; with a little training and some expert guidance they were soon able to produce Z specifications. Nearly all the institutions who have used Z intend to do so again; those who don’t plan to use a formal method more appropriate to their needs. We did not uncover many really large projects using Z, but most of those which we did survey are of a reasonable size. Over half the projects surveyed are using tools, with the majority of them employing type checking support. Tools use grows with the size of the project, although several large specifications have been produced without the use of tools. Not many people are proving their specifications, nor stating desirable theorems or proof obligations. However, many people expressed an interest in this with the unavailability of appropriate tool support being given as a reason for not attempting proof.