A transformational language for mutant description

Mutation testing has been used to assess the quality of test case suites by analyzing the ability in distinguishing the artifact under testing from a set of alternative artifacts, the so-called mutants. The mutants are generated from the artifact under testing by applying a set of mutant operators, which produce artifacts with simple syntactical differences. The mutant operators are usually based on typical errors that occur during the software development and can be related to a fault model. In this paper, we propose a language-named MuDeL (MUtant DEfinition Language)-for the definition of mutant operators, aiming not only at automating the mutant generation, but also at providing precision and formality to the operator definition. The proposed language is based on concepts from transformational and logical programming paradigms, as well as from context-free grammar theory. Denotational semantics formal framework is employed to define the semantics of the MuDeL language. We also describe a system-named mudelgen-developed to support the use of this language. An executable representation of the denotational semantics of the language is used to check the correctness of the implementation of mudelgen. At the very end, a mutant generator module is produced, which can be incorporated into a specific mutant tool/environment. (C) 2008 Elsevier Ltd. All rights reserved.

Language and interaction in online asynchronous communication in university level English courses

Interaction involves people communicating and reacting to each other. This process is key to the study of discourse, but it is not easy to study systematically how interaction takes place in a specific communicative event, or how it is typically performed over a series of repeated communicative events. However, with a written record of the interaction, it becomes possible to study the process in some detail. This thesis investigates interaction through asynchronous written discussion forums in a computer-mediated learning environment. In particular, this study investigates pragmatic aspects of the communicative event which the asynchronous online discussions comprise. The first case study examines response patterns to messages by looking at the content of initial messages and responses, in order to determine the extent to which characteristics of the messages themselves or other situational factors affect the interaction. The second study examines in what ways participants use a range of discourse devices, including formulaic politeness, humour and supportive feedback as community building strategies in the interaction. The third study investigates the role of the subject line of messages in the interaction, for example by examining how participants choose different types of subject lines for different types of messages. The fourth study examines to what extent features serving a deictic function are drawn on in the interaction and then compares the findings to both oral conversation and formal academic discourse. The overall findings show a complex communicative situation shaped by the medium itself, type of activity, the academic discipline and topic of discussion and by the social and cultural aspects of tertiary education in an online learning environment. In addition, the findings may also provide evidence of learning.  

Design and use of mobile technology in distance language education : Matching learning practices with technologies-in-practice

This thesis focuses on the adaptation of formal education to people’s technology- use patterns, theirtechnology-in-practice, where the ubiquitous use of mobile technologies is central. The research question is: How can language learning practices occuring in informal learning environments be effectively integrated with formal education through the use of mobile technology? The study investigates the technical, pedagogical, social and cultural challenges involved in a design science approach. The thesis consists of four studies. The first study systematises MALL (mobile-assisted language learning) research. The second investigates Swedish and Chinese students’ attitudes towards the use of mobile technology in education. The third examines students’ use of technology in an online language course, with a specific focus on their learning practices in informal learning contexts and their understanding of how this use guides their learning. Based on the findings, a specifically designed MALL application was built and used in two courses. Study four analyses the app use in terms of students’ perceived level of self-regulation and structuration. The studies show that technology itself plays a very important role in reshaping peoples’ attitudes and that new learning methods are coconstructed in a sociotechnical system. Technology’s influence on student practices is equally strong across borders. Students’ established technologies-in-practice guide the ways they approach learning. Hence, designing effective online distance education involves three interrelated elements: technology, information, and social arrangements. This thesis contributes to mobile learning research by offering empirically and theoretically grounded insights that shift the focus from technology design to design of information systems.

Community language programs in Australian schools: policy at the crossroads

The linguistic situation in Australia today presents an intriguing case for sociolinguistic inquiries. Despite the recent waves of migration from non Anglo-Celtic regions, the majority of Australians today are primarily monolingual with English being the dominant language. More critical, perhaps, is the diminishing appeal of second language learning even among second generation speakers of the large ethnic communities. This is indeed ironic giving that prior to white settlement in Australia, the Aboriginal inhabitants were predominantly multilingual with more than 250 languages (and many of their dialects) spoken by the 300 000 original inhabitants at the time when Captain James Cook's ship reached Botany Bay in Sydney in 1770. Given the size of the post-War migration, it was not until 1987 that the Australian government adopted a formal national policy on languages becoming 'the first English-speaking country to have such a policy and the first in the world to have a multilingual languages policy' (Australian Alliance for Languages 2001: 2). This paper will discuss the historical context for multilingualism in Australia and the current trend in government policy and funding. It will provide insights into community language programs and the challenges of remaining viable and relevant in the current social and political climate. Statistical analyses will be used to highlight emerging trends and future prospects.

Are we speaking the same language? Corporate perceptions of human rights responsibilities

Over the last several years, notions of corporate social responsibility and corporate responsibility for human rights have developed on several fronts, including under international human rights law, through voluntary initiatives and in the discourse and the reporting of the corporations themselves. But are all protagonists on all these fronts speaking the same language? Are these developments truly improving the realisation of human rights?
As one aspect of its three year Australian Research Council project examining the legal human rights responsibilities of multinational corporations, the Castan Centre for Human Rights Law set out to discover the perceptions that multinational corporations have of their own human rights responsibilities, the types of activities undertaken by corporations to fulfill those responsibilities and the appropriate extent, if any, of the imposition of legally binding human rights obligations on corporations.
While not setting out the formal findings of that empirical study, this paper reports on some interesting discoveries as to how corporations see their place in the human rights debate. It notes a divergence among corporations' views of the nature of human rights responsibility - whether an obligation or a benevolence - as well as its content. In considering whether corporations ought to have legally binding human rights obligations, a surprising number of corporations replied in the affirmative, citing reasons such as certainty in dealing with suppliers and instituting a level playing field against rogue operators.
However,  perhaps the most important finding is the different understandings of human rights as they relate to a corporation's operations. Agreement on potential reforms would be meaningless if they were not employed towards a commonly understood end. After examining the various responses of the corporations and the evidence they cited to support their contentions, the paper concludes that the various protagonists of human rights responsibility for corporations may be using the same words, but they are not yet speaking the same language.

Conceptual complexity and apparent contradictions in mathematics language

The article explores the conceptual complexity and apparent contradictions in the language of mathematics and suggests ways to handle these problems. Mathematics, as described the author, is a formal, artificially constructed language. One problem arises from the changes of gradient and rates of change of gradient, continuous functions. Conceptual conflicts also arise when least upperbounds and greatest lower-bounds in discussing sequences and series, convergence and limits are considered.

Fuzzy concepts and formal methods

It has been recognised that formal methods are useful as a modelling tool in requirements engineering. Specification languages such as Z permit the precise and unambiguous modelling of system properties and behaviour. However some system problems, particularly those drawn from the information systems problem domain, may be difficult to model in crisp or precise terms. It may also be desirable that formal modelling should commence as early as possible, even when our understanding of parts of the problem domain is only approximate. This thesis suggests fuzzy set theory as a possible representation scheme for this imprecision or approximation. A fuzzy logic toolkit that defines the operators, measures and modifiers necessary for the manipulation of fuzzy sets and relations is developed. The toolkit contains a detailed set of laws that demonstrate the properties of the definitions when applied to partial set membership. It also provides a set of laws that establishes an isomorphism between the toolkit notation and that of conventional Z when applied to boolean sets and relations. The thesis also illustrates how the fuzzy logic toolkit can be applied in the problem domains of interest. Several examples are presented and discussed including the representation of imprecise concepts as fuzzy sets and relations, system requirements as a series of linguistically quantified propositions, the modelling of conflict and agreement in terms of fuzzy sets and the partial specification of a fuzzy expert system. The thesis concludes with a consideration of potential areas for future research arising from the work presented here.

Heteroglossia : a space for developing critical language awareness?

This paper reports on research into the challenges of implementing a critical writing pedagogy within a teacher education program in Australia. Participants in this study are student teachers enrolled in a compulsory subject, ‘Language and Literacy in Secondary School’, a subject requiring them to develop a knowledge of the role of language and literacy across the secondary school curriculum and to show personal proficiency in literacy (this is dictated by state government specifications of graduate outcomes for teacher education programs). To develop an understanding of the way that language has shaped their lives, students write a narrative about their early literacy experiences – a task which they all find very challenging, especially in comparison with the formal writing of other university subjects. Rather than simply reminiscing about their early childhood, they are encouraged to juxtapose voices from the past and the present, and to combine a range of texts within their writing. They thereby create a heteroglossic text (Bakhtin, 1981) that stretches their repertoires as language users and enables them to develop a socially critical awareness of language and literacy, including the literacy practices in which they engage as university students. Later in the semester they revisit these accounts of their early literacy experiences, and (in a separate piece of writing) endeavour to place these accounts within the contexts of theories and debates they have encountered in the course of completing this unit.

The students’ writing provides a small window on how they are experiencing their tertiary education, including the managerial controls that are currently shaping university curriculum and pedagogy. Their writing also raises questions as to extent to which tertiary students are actually able to formulate a critical language awareness that will subsequently inform their professional practice as secondary teachers.

Heteroglossia : a space for developing critical language awareness?

This paper reports on research into the challenges of implementing a critical writing pedagogy within a teacher education program in Australia. Participants in this study are student teachers enrolled in a compulsory subject, “Language and Literacy in Secondary School”, a subject requiring them to develop a knowledge of the role of language and literacy across the secondary school curriculum and to show personal proficiency in literacy as part of graduate outcomes for teacher education dictated by the State Government of Victoria. To develop an understanding of the way that language has shaped their lives, students write a narrative about their early literacy experiences – a task which they all find very challenging, especially in comparison with the formal writing of other university subjects. Rather than simply reminiscing about their early childhood, they are encouraged to juxtapose voices from the past and the present, and to combine a range of texts within their writing. Later in the semester they revisit these accounts of their early literacy experiences and, in a separate piece of writing, endeavour to place these accounts within the contexts of theories and debates they have encountered in the course of completing this unit. The students’ writing provides a small window on how they are experiencing their tertiary education and their preparation as teachers, including the managerial controls that are currently shaping university curriculum and pedagogy. We argue that such heteroglossic texts (Bakhtin, 1981) prompt students to stretch their repertoires as language-users, enabling them to develop a socially critical awareness of language and literacy, including the literacy practices in which they engage as university students.

Semântica formal para TVQL

Modelos de bancos de dados têm sido progressivamente estendidos a fim de melhor capturar necessidades específicas de aplicações. Bancos de dados versionados, por exemplo, provêm suporte a versões alternativas de objetos. Bancos de dados temporais, por sua vez, permitem armazenar todos os estados de uma aplicação, registrando sua evolução com o passar do tempo. Tais extensões sobre os modelos de dados se refletem nas respectivas linguagens de consulta, normalmente sob a forma de extensões a linguagens conhecidas, tais como SQL ou OQL. O modelo de banco de dados TVM (Temporal Versions Model ), definido sobre o modelo de banco de dados orientado a objetos, suporta simultaneamente versões alternativas e o registro de alterações de objetos ao longo do tempo. A linguagem de consulta TVQL (Temporal Versioned Query Language), definida a partir da linguagem de consulta SQL, permite recuperar informações do modelo de dados TVM. As construções introduzidas em TVQL têm como objetivo tornar simples a consulta do banco de dados em diversos pontos da linha temporal. Apesar das vantagens da utilização da linguagem TVQL para resgatar dados temporais do modelo TVM, existem algumas limitações importantes para seu aprimoramento. Uma delas é a alta complexidade do modelo TVM, proveniente da integração de conceitos variados como estados alternativos e rótulos temporais. Outro ponto é que, até o presente momento, não existe um interpretador para TVQL, impedindo uma experiência prática de programação de consultas. O objetivo principal deste trabalho é o desenvolvimento de uma especificação formal para a linguagem TVQL, tornando possível um estudo consistente de suas construções. Adicionalmente, uma especificação formal serve como documentação para futuras implementações de interpretadores. Neste trabalho foi desenvolvido um protótipo de avaliador de consultas e verificador de tipos para um núcleo funcional da linguagem TVQL, possibilitando também uma experimentação prática sobre os modelos propostos.

JML- Based formal development of a Java card application for managing medical appointments

Although formal methods can dramatically increase the quality of software systems, they have not widely been adopted in software industry. Many software companies have the perception that formal methods are not cost-effective cause they are plenty of mathematical symbols that are difficult for non-experts to assimilate. The Java Modelling Language (short for JML) Section 3.3 is an academic initiative towards the development of a common formal specification language for Java programs, and the implementation of tools to check program correctness. This master thesis work shows how JML based formal methods can be used to formally develop a privacy sensitive Java application. This is a smart card application for managing medical appointments. The application is named HealthCard. We follow the software development strategy introduced by João Pestana, presented in Section 3.4. Our work influenced the development of this strategy by providing hands-on insight on challenges related to development of a privacy sensitive application in Java. Pestana’s strategy is based on a three-step evolution strategy of software specifications, from informal ones, through semiformal ones, to JML formal specifications. We further prove that this strategy can be automated by implementing a tool that generates JML formal specifications from a welldefined subset of informal software specifications. Hence, our work proves that JML-based formal methods techniques are cost-effective, and that they can be made popular in software industry. Although formal methods are not popular in many software development companies, we endeavour to integrate formal methods to general software practices. We hope our work can contribute to a better acceptance of mathematical based formalisms and tools used by software engineers. The structure of this document is as follows. In Section 2, we describe the preliminaries of this thesis work. We make an introduction to the application for managing medical applications we have implemented. We also describe the technologies used in the development of the application. This section further illustrates the Java Card Remote Method Invocation communication model used in the medical application for the client and server applications. Section 3 introduces software correctness, including the design by contract and the concept of contract in JML. Section 4 presents the design structure of the application. Section 5 shows the implementation of the HealthCard. Section 6 describes how the HealthCard is verified and validated using JML formal methods tools. Section 7 includes some metrics of the HealthCard implementation and specification. Section 8 presents a short example of how a client-side of a smart card application can be implemented while respecting formal specifications. Section 9 describes a prototype tools to generate JML formal specifications from informal specifications automatically. Section 10 describes some challenges and main ideas came acrorss during the development of the HealthCard. The full formal specification and implementation of the HealthCard smart card application presented in this document can be reached at https://sourceforge.net/projects/healthcard/.

A JML-Based strategy for incorporating formal specifications into the software development process

This thesis presents a JML-based strategy that incorporates formal specifications into the software development process of object-oriented programs. The strategy evolves functional requirements into a “semi-formal” requirements form, and then expressing them as JML formal specifications. The strategy is implemented as a formal-specification pseudo-phase that runs in parallel with the other phase of software development. What makes our strategy different from other software development strategies used in literature is the particular use of JML specifications we make all along the way from requirements to validation-and-verification.

Uma arquitetura baseada em SCTP e SIP para suporte a aplicações VoIP móveis e a especificação formal do seu módulo de controle

New versions of SCTP protocol allow the implementation of handover procedures in the transport layer, as well as the supply of a partially reliable communication service. A communication architecture is proposed herein, integrating SCTP with the session initiation protocol, SIP, besides additional protocols. This architecture is intended to handle voice applications over IP networks with mobility requirements. User localization procedures are specified in the application layer as well, using SIP, as an alternative mean to the mechanisms used by traditional protocols, that support mobility in the network layer. The SDL formal specification language is used to specify the operation of a control module, which coordinates the operation of the system component protocols. This formal specification is intended to prevent ambiguities and inconsistencies in the definition of this module, assisting in the correct implementation of the elements of this architecture

JCML - Java Card Modeling Language: Definição e Implementação

Formal methods should be used to specify and verify on-card software in Java Card applications. Furthermore, Java Card programming style requires runtime verification of all input conditions for all on-card methods, where the main goal is to preserve the data in the card. Design by contract, and in particular, the JML language, are an option for this kind of development and verification, as runtime verification is part of the Design by contract method implemented by JML. However, JML and its currently available tools for runtime verification were not designed with Java Card limitations in mind and are not Java Card compliant. In this thesis, we analyze how much of this situation is really intrinsic of Java Card limitations and how much is just a matter of a complete re-design of JML and its tools. We propose the requirements for a new language which is Java Card compliant and indicate the lines on which a compiler for this language should be built. JCML strips from JML non-Java Card aspects such as concurrency and unsupported types. This would not be enough, however, without a great effort in optimization of the verification code generated by its compiler, as this verification code must run on the card. The JCML compiler, although being much more restricted than the one for JML, is able to generate Java Card compliant verification code for some lightweight specifications. As conclusion, we present a Java Card compliant variant of JML, JCML (Java Card Modeling Language), with a preliminary version of its compiler

BSmart: desenvolvimento rigoroso de aplicações Java Card com base no método formal B

Java Card technology allows the development and execution of small applications embedded in smart cards. A Java Card application is composed of an external card client and of an application in the card that implements the services available to the client by means of an Application Programming Interface (API). Usually, these applications manipulate and store important information, such as cash and confidential data of their owners. Thus, it is necessary to adopt rigor on developing a smart card application to improve its quality and trustworthiness. The use of formal methods on the development of these applications is a way to reach these quality requirements. The B method is one of the many formal methods for system specification. The development in B starts with the functional specification of the system, continues with the application of some optional refinements to the specification and, from the last level of refinement, it is possible to generate code for some programming language. The B formalism has a good tool support and its application to Java Card is adequate since the specification and development of APIs is one of the major applications of B. The BSmart method proposed here aims to promote the rigorous development of Java Card applications up to the generation of its code, based on the refinement of its formal specification described in the B notation. This development is supported by the BSmart tool, that is composed of some programs that automate each stage of the method; and by a library of B modules and Java Card classes that model primitive types, essential Java Card API classes and reusable data structures