Towards platform-independent real-time systems

Real-time software systems are rarely developed once and left to run. They are subject to changes of requirements as the applications they support expand, and they commonly outlive the platforms they were designed to run on. A successful real-time system is duplicated and adapted to a variety of applications - it becomes a product line. Current methods for real-time software development are commonly based on low-level programming languages and involve considerable duplication of effort when a similar system is to be developed or the hardware platform changes. To provide more dependable, flexible and maintainable real-time systems at a lower cost what is needed is a platform-independent approach to real-time systems development. The development process is composed of two phases: a platform-independent phase, that defines the desired system behaviour and develops a platform-independent design and implementation, and a platform-dependent phase that maps the implementation onto the target platform. The last phase should be highly automated. For critical systems, assessing dependability is crucial. The partitioning into platform dependent and independent phases has to support verification of system properties through both phases.

Interfacing ASM with the MDG tool

In this paper we describe an approach to interface Abstract State Machines (ASM) with Multiway Decision Graphs (MDG) to enable tool support for the formal verification of ASM descriptions. ASM is a specification method for software and hardware providing a powerful means of modeling various kinds of systems. MDGs are decision diagrams based on abstract representation of data and axe used primarily for modeling hardware systems. The notions of ASM and MDG axe hence closely related to each other, making it appealing to link these two concepts. The proposed interface between ASM and MDG uses two steps: first, the ASM model is transformed into a flat, simple transition system as an intermediate model. Second, this intermediate model is transformed into the syntax of the input language of the MDG tool, MDG-HDL. We have successfully applied this transformation scheme on a case study, the Island Tunnel Controller, where we automatically generated the corresponding MDG-HDL models from ASM specifications.

Conceptual Model and Security Requirements for DRM Techniques Used for e-Learning Objects Protection

This paper deals with the security problems of DRM protected e-learning content. After a short review of the main DRM systems and methods used in e-learning, an examination is made of participators in DRM schemes (e-learning object author, content creator, content publisher, license creator and end user). Then a conceptual model of security related processes of DRM implementation is proposed which is improved afterwards to reflect some particularities in DRM protection of e-learning objects. A methodical way is used to describe the security related motives, responsibilities and goals of the main participators involved in the DRM system. Taken together with the process model, these security properties are used to establish a list of requirements to fulfill and a possibility for formal verification of real DRM systems compliance with these requirements.

An integrated framework for ensuring the quality of software design

Software development is an extremely complex process, during which human errors are introduced and result in faulty software systems. It is highly desirable and important that these errors can be prevented and detected as early as possible. Software architecture design is a high-level system description, which embodies many system features and properties that are eventually implemented in the final operational system. Therefore, methods for modeling and analyzing software architecture descriptions can help prevent and reveal human errors and thus improve software quality. Furthermore, if an analyzed software architecture description can be used to derive a partial software implementation, especially when the derivation can be automated, significant benefits can be gained with regard to both the system quality and productivity. This dissertation proposes a framework for an integrated analysis on both of the design and implementation. To ensure the desirable properties of the architecture model, we apply formal verification by using the model checking technique. To ensure the desirable properties of the implementation, we develop a methodology and the associated tool to translate an architecture specification into an implementation written in the combination of Arch-Java/Java/AspectJ programming languages. The translation is semi-automatic so that many manual programming errors can be prevented. Furthermore, the translation inserting monitoring code into the implementation such that runtime verification can be performed, this provides additional assurance for the quality of the implementation. Moreover, validations for the translations from architecture model to program are provided. Finally, several case studies are experimented and presented.

JCML: A specification language for the runtime verification of Java Card programs

COSTA, Umberto Souza; MOREIRA, Anamaria Martins; MUSICANTE, Matin A.; SOUZA NETO, Plácido A. JCML: A specification language for the runtime verification of Java Card programs. Science of Computer Programming. [S.l]: [s.n], 2010.

Specification and Runtime Verification of Java Card Programs

COSTA, Umberto Souza da; MOREIRA, Anamaria Martins; MUSICANTE, Martin A. Specification and Runtime Verification of Java Card Programs. Electronic Notes in Theoretical Computer Science. [S.l:s.n], 2009.

Grounded Theory methods in child psychotherapy research

This article considers the place of qualitative research in psychoanalysis and child psychotherapy. It discusses why research methodology for many years occupied so small a place in these fields, and examines the cultural and social developments since the 1960s which have changed this situation, giving formal methods of research much greater significance. It reflects on the different pressures to develop formal research methods which arise both from outside the psychoanalytic field, as a condition of its continued professional survival, and from within it, where its main aim is the development of fundamental psychoanalytic knowledge, It suggests that the conduct of mainly quantitative research into treatment outcomes is largely a response to these external pressures, whilst the main benefits to be gained from the development of qualitative research methods, such as Grounded Theory, are in facilitating the knowledge-generating capacities and achievements of child psychotherapists themselves. The paper describes Grounded Theory methods, and explains how they can be valuable in the recognition of hitherto unrecognised meanings and patterns as these are made visible in clinical practice. Finally, it briefly describes five different examples of completed doctoral studies, all of which have added significantly to the knowledge-base of child psychotherapy, and which demonstrate how much can be accomplished using this method of research.

JCML: A specification language for the runtime verification of Java Card programs

COSTA, Umberto Souza; MOREIRA, Anamaria Martins; MUSICANTE, Matin A.; SOUZA NETO, Plácido A. JCML: A specification language for the runtime verification of Java Card programs. Science of Computer Programming. [S.l]: [s.n], 2010.

Specification and Runtime Verification of Java Card Programs

COSTA, Umberto Souza da; MOREIRA, Anamaria Martins; MUSICANTE, Martin A. Specification and Runtime Verification of Java Card Programs. Electronic Notes in Theoretical Computer Science. [S.l:s.n], 2009.

The efficacy of waste management plans in Australian commercial construction refurbishment projects

Renovation and refurbishment of the existing commercial building stock is a growing area of total construction activity and a significant generator of waste sent to landfill in Australia. A written waste management plan (WMP) is a widespread regulatory requirement for commercial office redevelopment projects. There is little evidence, however, that WMPs actually increase the quantity of waste that is ultimately diverted from landfill. Some reports indicate an absence of any formal verification or monitoring process by regulators to assess the efficacy of the plans. In order to gauge the extent of the problem a survey was conducted of twenty four consultants and practitioners involved in commercial office building refurbishment projects to determine the state of current practice with regard to WMPs and to elicit suggestions with regard to ways of making the process more effective. Considerable variation in commitment to recycling policies was encountered indicating a need to revisit waste minimisation practices if the environmental performance of refurbishment projects is to be improved.

Making a match: Combining theory and evidence in policy-oriented macroeconomic modeling

A persistent question in the development of models for macroeconomic policy analysis has been the relative role of economic theory and evidence in their construction. This paper looks at some popular strategies that involve setting up a theoretical or conceptual model (CM) which is transformed to match the data and then made operational for policy analysis. A dynamic general equilibrium model is constructed that is similar to standard CMs. After calibration to UK data it is used to examine the utility of formal econometric methods in assessing the match of the CM to the data and also to evaluate some standard model-building strategies. Keywords: Policy oriented economic modeling; Model evaluation; VAR models

Evaluation of the year 1 literacy and numeracy checkpoints assessments trial - 2010

The draft Year 1 Literacy and Numeracy Checkpoints Assessments were in open and supported trial during Semester 2, 2010. The purpose of these trials was to evaluate the Year 1 Literacy and Numeracy Checkpoints Assessments (hereafter the Year 1 Checkpoints) that were designed in 2009 as a way to incorporate the use of the Year 1 Literacy and Numeracy Indicators as formative assessment in Year 1 in Queensland Schools. In these trials there were no mandated reporting requirements. The processes of assessment were related to future teaching decisions. As such the trials were trials of materials and the processes of using those materials to assess students, plan and teach in year 1 classrooms. In their current form the Year 1 Checkpoints provide assessment resources for teachers to use in February, June and October. They aim to support teachers in monitoring children's progress and making judgments about their achievement of the targeted P‐3 Literacy and Numeracy Indicators by the end of Year 1 (Queensland Studies Authority, 2010 p. 1). The Year 1 Checkpoints include support materials for teachers and administrators, an introductory statement on assessment, work samples, and a Data Analysis Assessment Record (DAAR) to record student performance. The Supported Trial participants were also supported with face‐to‐face and on‐line training sessions, involvement in a moderation process after the October Assessments, opportunities to participate in discussion forums as well as additional readings and materials. The assessment resources aim to use effective early years assessment practices in that the evidence is gathered from hands‐on teaching and learning experiences, rather than more formal assessment methods. They are based in a model of assessment for learning, and aim to support teachers in the “on‐going process of determining future learning directions” (Queensland Studies Authority, 2010 p. 1) for all students. Their aim is to focus teachers on interpreting and analysing evidence to make informed judgments about the achievement of all students, as a way to support subsequent planning for learning and teaching. The Evaluation of the Year 1 Literacy and Numeracy Checkpoints Assessments Supported Trial (hereafter the Evaluation) aimed to gather information about the appropriateness, effectiveness and utility of the Year 1 Checkpoints Assessments from early years’ teachers and leaders in up to one hundred Education Queensland schools who had volunteered to be part of the Supported Trial. These sample schools represent schools across a variety of Education Queensland regions and include schools with:  - A high Indigenous student population; - Urban, rural and remote school locations; - Single and multi‐age early phase classes; - A high proportion of students from low SES backgrounds. The purpose of the Evaluation was to: Evaluate the materials and report on the views of school‐based staff involved in the trial on the process, materials, and assessment practices utilised. The Evaluation has reviewed the materials, and used surveys, interviews, and observations of processes and procedures to collect relevant data to help present an informed opinion on the Year 1 Checkpoints as assessment for the early years of schooling. Student work samples and teacher planning and assessment documents were also collected. The evaluation has not evaluated the Year 1 Checkpoints in any other capacity than as a resource for Year 1 teachers and relevant support staff.

Analysis of Object-Specific Authorization Protocol (OSAP) using coloured Petri nets

The use of Trusted Platform Module (TPM) is be- coming increasingly popular in many security sys- tems. To access objects protected by TPM (such as cryptographic keys), several cryptographic proto- cols, such as the Object Specific Authorization Pro- tocol (OSAP), can be used. Given the sensitivity and the importance of those objects protected by TPM, the security of this protocol is vital. Formal meth- ods allow a precise and complete analysis of crypto- graphic protocols such that their security properties can be asserted with high assurance. Unfortunately, formal verification of these protocols are limited, de- spite the abundance of formal tools that one can use. In this paper, we demonstrate the use of Coloured Petri Nets (CPN) - a type of formal technique, to formally model the OSAP. Using this model, we then verify the authentication property of this protocol us- ing the state space analysis technique. The results of analysis demonstrates that as reported by Chen and Ryan the authentication property of OSAP can be violated.

Timed and Probabilistic Automata for Automatic Animal Call Recognition

Automatic Call Recognition is vital for environmental monitoring. Patten recognition has been applied in automatic species recognition for years. However, few studies have applied formal syntactic methods to species call structure analysis. This paper introduces a novel method to adopt timed and probabilistic automata in automatic species recognition based upon acoustic components as the primitives. We demonstrate this through one kind of birds in Australia: Eastern Yellow Robin.

Ontology-based feature modeling for construction information extraction from a building information model

A building information model (BIM) provides a rich representation of a building's design. However, there are many challenges in getting construction-specific information from a BIM, limiting the usability of BIM for construction and other downstream processes. This paper describes a novel approach that utilizes ontology-based feature modeling, automatic feature extraction based on ifcXML, and query processing to extract information relevant to construction practitioners from a given BIM. The feature ontology generically represents construction-specific information that is useful for a broad range of construction management functions. The software prototype uses the ontology to transform the designer-focused BIM into a construction-specific feature-based model (FBM). The formal query methods operate on the FBM to further help construction users to quickly extract the necessary information from a BIM. Our tests demonstrate that this approach provides a richer representation of construction-specific information compared to existing BIM tools.