This innovative practice, work in progress paper investigates constructive alignment in a first-year engineering course. Constructive alignment describes a course environment where stated course outcomes are in alignment with what students learn in the course. This study develops a novel method to explore the extent of constructive alignment. Drawing on minute papers which were already incorporated in the course, the study uses student responses to a final minute paper which required students to reflect briefly on what they learned in the course. Qualitative analysis of 189 responses determined four main themes, with two of them featuring prominently in some detail: teamwork and problem-solving. This was important evidence of alignment as these are key outcomes of this project-centered course. A further interesting finding was that students see programming as a focus for their learning but don't explicitly link it to the modeling of an engineering system as stated in the course learning outcomes.

Background: The accurate prediction of where faults are likely to occur in code can help direct test effort, reduce costs, and improve the quality of software. Objective: We investigate how the context of models, the independent variables used, and the modeling techniques applied influence the performance of fault prediction models. Method: We used a systematic literature review to identify 208 fault prediction studies published from January 2000 to December 2010. We synthesize the quantitative and qualitative results of 36 studies which report sufficient contextual and methodological information according to the criteria we develop and apply. Results: The models that perform well tend to be based on simple modeling techniques such as Naive Bayes or Logistic Regression. Combinations of independent variables have been used by models that perform well. Feature selection has been applied to these combinations when models are performing particularly well. Conclusion: The methodology used to build models seems to be influential to predictive performance. Although there are a set of fault prediction studies in which confidence is possible, more studies are needed that use a reliable methodology and which report their context, methodology, and performance comprehensively.

Security protocols are often analysed in isolation as academic challenges. However, the real world can require various combinations of them, such as a certified email protocol executed over a resilient channel, or the key registration protocol to precede the purchase protocols of Secure Electronic Transactions (SET). We develop what appears to be the first scalable approach to specifying and analysing mix protocols. It expands on the Inductive Method by exploiting the simplicity with which inductive definitions can refer to each other. This lets the human analyst study each protocol separately first, and then derive holistic properties about the mix. The approach, which is demonstrated on the sequential composition of a certification protocol with an authentication one, is not limited by the features of the protocols, which can, for example, share message components such as cryptographic keys and nonces. It bears potential for the analysis of complex protocols constructed by general composition of others.

Background: The NASA Metrics Data Program data sets have been heavily used in software defect prediction experiments. Aim: To demonstrate and explain why these data sets require significant pre-processing in order to be suitable for defect prediction. Method: A meticulously documented data cleansing process involving all 13 of the original NASA data sets. Results: Post our novel data cleansing process; each of the data sets had between 6 to 90 percent less of their original number of recorded values. Conclusions: One: Researchers need to analyse the data that forms the basis of their findings in the context of how it will be used. Two: Defect prediction data sets could benefit from lower level code metrics in addition to those more commonly used, as these will help to distinguish modules, reducing the likelihood of repeated data points. Three: The bulk of defect prediction experiments based on the NASA Metrics Data Program data sets may have led to erroneous findings. This is mainly due to repeated data points potentially causing substantial amounts of training and testing data to be identical.

Background: There has been much discussion amongst auto-mated software defect prediction researchers regarding use of the precision and false positive rate classifier performance metrics. Aim: To demonstrate and explain why failing to report precision when using data with highly imbalanced class distributions may provide an overly optimistic view of classifier performance. Method: Well documented examples of how dependent class distribution affects the suitability of performance measures. Conclusions: When using data where the minority class repre-sents less than around 5 to 10 percent of data points in total, failing to report precision may be a critical mistake. Furthermore, deriving the precision values omitted from studies can reveal valuable insight into true classifier performance. I.

Many studies have been carried out to predict the presence of software code defects using static code metrics. Such studies typically report how a classifier performs with real world data, but usually no analysis of the predictions is carried out. An analysis of this kind may be worthwhile as it can illuminate the motivation behind the predictions and the severity of the misclassifications. This investigation involves a manual analysis of the predictions made by Support Vector Machine classifiers using data from the NASA Metrics Data Program repository. The findings show that the predictions are generally well motivated and that the classifiers were, on average, more “confident” in the predictions they made which were correct.

Predicting the rate at which a substance will pass through human skin and into the bloodstream is a problem of current interest. We use Gaussian Process modeling to train a set of predictors using every combination of six molecular features. We find that only three of the features are needed for our best predictor. This result could be useful in the further analysis of skin permeability.

In this paper we describe a sighting blurring algorithm for use by a trusted middleware infrastructure, which is part of an architecture that supports the operation of Location Based Services (LBSs) over the Internet. This infrastructure can only obtain sightings for the users who are directly involved in a current invocation of an LBS. Therefore, our sighting blurring algorithm is designed to be dependent on only the sightings of these users. Our sighting blurring algorithm offers these users increased privacy by performing spatial blurring on the location components of their sightings. It does not perform temporal blurring, because we believe that this reduces an LBS's ability to offer a useful service. Instead, our sighting blurring algorithm introduces a new parameter that specifies the frequency with which sightings are released by the infrastructure for a particular user. This frequency parameter is a function of the size of the location component.

The prime number theorem, established by Hadamard and de la Vallée Poussin independently in 1896, asserts that the density of primes in the positive integers is asymptotic to 1/ln x . Whereas their proofs made serious use of the methods of complex analysis, elementary proofs were provided by Selberg and Erdös in 1948. We describe a formally verified version of Selberg's proof, obtained using the Isabelle proof assistant.

Motivated by pseudonym management in a Location-Based Services (LBS) platform, we describe a mediated identity-based encryption (mIBE) scheme that can be used to protect identities and communications in this environment. We introduce a process whereby a mobile user is only required to own one priva te key in order to protect their communications when accessing LBS under different pseudonyms. The identity-based character of the scheme simplifies key management by removing the need for digital certificates and the mediated architecture allows for simple, instant key revocation.

A specification, and its development, for a small bookshop information system are discussed. the specification is presented using mathematics and the scheme calculus of C. Morgan and B. Sufrin (see ibid., vol.SE-10, no.2, p.128-142, 1984). An insight is given into how the specification was developed and why a formal specification is appropriate.>