At the end of September, my colleague presented three short (works-in-progress) papers at AVoCS 2014, the 14th International Workshop on Automated Verification of Critical Systems at the University of Twente in the Netherlands. This presents some of our recent work on code verification, restricting typing and source code annotations for effective software engineering.
The abstracts of the three papers are as follows; you can also download the full proceedings:
Efficacy Measurement of Early Intervention Techniques
Dave Donaghy and Tom Crick
Compiler technology has, for some considerable time, been sufficiently advanced that individual programmers are able to produce, in reasonably short periods of time, tools that might aid with the development process in novel ways: for example, one can easily produce a C compiler tool that will detect uncommon uses of integer arithmetic (such as the rare multiplication of values that are commonly only added) and flag such uses as potential errors. However, there is currently no convenient way to measure the efficacy of such techniques: where one might assume that uncommon uses of integer arithmetic might be erroneous, we do not have a way of measuring the cost saving associated with the potential early detection of occurrences of such things. We present a method of measuring the efficacy of a single early intervention, based on the replaying of previous executions of a compile-build-test cycle. This measurement process allows us to identify the software errors that were introduced during an original development and subsequently fixed; additionally, it allows us to identify the subset of such errors that would have been identified by the early intervention. By these means, we can take an existing historical record of a development, and extract from it meaningful information about the value of a proposed new early intervention technique.
No-Test Classes in C through Restricted Types
Dave Donaghy and Tom Crick
Object-oriented programming (OOP) languages allow for the creation of rich new types through, for example, the class mechanism found in C++ and Python (among others). These techniques, while certainly rich in the functionality they provide, additionally require users to develop and test new types; while resulting software can be elegant and easy to understand (and indeed these were some of the aspirations behind the OOP paradigm), there is a cost associated to the addition of the new code required to implement such new types. Such a cost will typically be at least linear in the number of new types introduced. One potential alternative to the creation of new types through extension is the creation of new types through restriction; in appropriate circumstances, such types can provide the same elegance and ease of understanding, but without a corresponding linear development and maintenance cost.
Physical Type Tracking through Minimal Source-Code Annotation
Dave Donaghy and Tom Crick
One of many common artefacts of complex software systems that often needs to be tracked through the entirety of the software system is the underlying type to which numerical variables refer. Commonly-used languages used in industry provide complex mechanisms through which general objects are associated to a given type: for example, the class (and template) mechanisms in Python (and C++) are extremely rich mechanisms for the construction of types with almost entirely arbitrary associated operation sets. However, one often deals with software objects that ultimately represent numerical entities corresponding to real-world measurements, even through standardised SI units: metres per second, kilogram metres per second-squared, etc. In such situations, one can be left with insufficient and ineffective type-checking: for example, the C double type will not prevent the erroneous addition of values representing velocity (with SI units metres per second) to values representing mass (SI unit kilogram). We present an addition to the C language, defined through the existing attribute mechanism, that allows automatic control of physical types at compile-time; the only requirement is that individual variables be identified at declaration time with appropriate SI (or similar) units.
(also see: Publications)
Digital, Data & Policy 