Integrating formal specification and software verification and validation

It is not surprising that students are unconvinced about the benefits of formal methods if we do not show them how these methods can be integrated with other activities in the software lifecycle. In this paper, we describe an approach to integrating formal specification with more traditional verification and validation techniques in a course that teaches formal specification and specification-based testing. This is accomplished through a series of assignments on a single software component that involves specifying the component in Object-Z, validating that specification using inspection and a specification animation tool, and then testing an implementation of the specification using test cases derived from the formal specification.

Gendered dichotomies and segregation patterns in computing jobs in Australia

Sex segregation in employment is a phenomenon that can be observed and analysed at different levels, ranging from comparisons between broad classifications by industry or occupation through to finely defined jobs within such classifications. From an aggregate perspective, the contribution of information technology (IT) employment to sex segregation is clear--it remains a highly male-dominated field apparently imbued with the ongoing masculinity of science and technology. While this situation is clearly contrary to hopes of a new industry freed from traditional distinctions between 'men's' and 'women's' work, it comes as little surprise to most feminist and labour studies analysts. An extensive literature documents the persistently masculine culture of IT employment and education (see, among many, Margolis and Fisher 2002; Wajcman 1991; Webster 1996; Wright 1996, 1997), and the idea that new occupations might escape sexism by sidestepping 'old traditions' has been effectively critiqued by writers such as Adam, who notes the fallacy of assuming a spontaneous emergence of equality in new settings (2005: 140).

A reference architecture for instructional educational software

Our extensive research has indicated that high-school teachers are reluctant to make use of existing instructional educational software (Pollard, 2005). Even software developed in a partnership between a teacher and a software engineer is unlikely to be adopted by teachers outside the partnership (Pollard, 2005). In this paper we address these issues directly by adopting a reusable architectural design for instructional educational software which allows easy customisation of software to meet the specific needs of individual teachers. By doing this we will facilitate more teachers regularly using instructional technology within their classrooms. Our domain-specific software architecture, Interface-Activities-Model, was designed specifically to facilitate individual customisation by redefining and restructuring what constitutes an object so that they can be readily reused or extended as required. The key to this architecture is the way in which the software is broken into small generic encapsulated components with minimal domain specific behaviour. The domain specific behaviour is decoupled from the interface and encapsulated in objects which relate to the instructional material through tasks and activities. The domain model is also broken into two distinct models - Application State Model and Domainspecific Data Model. This decoupling and distribution of control gives the software designer enormous flexibility in modifying components without affecting other sections of the design. This paper sets the context of this architecture, describes it in detail, and applies it to an actual application developed to teach high-school mathematical concepts.