A formal metamodeling approach to a transformation between the UML state machine and object-z

A significant problem with currently suggested approaches for transforming between models in different languages is that the transformation is often described imprecisely, with the result that the overall transformation task may be imprecise, incomplete and inconsistent. This paper presents a formal metamodeling approach for transforming between UML and Object-Z. In the paper, the two languages are defined in terms of their formal metamodels, and a systematic transformation between the models is provided at the meta-level in terms of formal mapping functions. As a consequence, we can provide a precise, consistent and complete transformation between them.

Formal derivation of finite state machines for class testing

Previous work on generating state machines for the purpose of class testing has not been formally based. There has also been work on deriving state machines from formal specifications for testing non-object-oriented software. We build on this work by presenting a method for deriving a state machine for testing purposes from a formal specification of the class under test. We also show how the resulting state machine can be used as the basis for a test suite developed and executed using an existing framework for class testing. To derive the state machine, we identify the states and possible interactions of the operations of the class under test. The Test Template Framework is used to formally derive the states from the Object-Z specification of the class under test. The transitions of the finite state machine are calculated from the derived states and the class's operations. The formally derived finite state machine is transformed to a ClassBench testgraph, which is used as input to the ClassBench framework to test a C++ implementation of the class. The method is illustrated using a simple bounded queue example.

Learning to play Pac-Man: An evolutionary, rule-based approach

Pac-Man is a well-known, real-time computer game that provides an interesting platform for research. We describe an initial approach to developing an artificial agent that replaces the human to play a simplified version of Pac-Man. The agent is specified as a simple finite state machine and ruleset. with parameters that control the probability of movement by the agent given the constraints of the maze at some instant of time. In contrast to previous approaches, the agent represents a dynamic strategy for playing Pac-Man, rather than a pre-programmed maze-solving method. The agent adaptively "learns" through the application of population-based incremental learning (PBIL) to adjust the agents' parameters. Experimental results are presented that give insight into some of the complexities of the game, as well as highlighting the limitations and difficulties of the representation of the agent.

Formal verification of ASM designs using the MDG tool

In this paper, we present a formal hardware verification framework linking ASM with MDG. ASM (Abstract State Machine) is a state based language for describing transition systems. MDG (Multiway Decision Graphs) provides symbolic representation of transition systems with support of abstract sorts and functions. We implemented a transformation tool that automatically generates MDG models from ASM specifications, then formal verification techniques provided by the MDG tool, such as model checking or equivalence checking, can be applied on the generated models. We support this work with a case study of an Island Tunnel Controller, which behavior and structure were specified in ASM then using our ASM-MDG tool successfully verified within the MDG tool.

Human behaviour modelled as a statistico-deterministic turing machine

'Free will' and its corollary, the concept of individual responsibility are keystones of the justice system. This paper shows that if we accept a physics that disallows time reversal, the concept of 'free will' is undermined by an integrated understanding of the influence of genetics and environment on human behavioural responses. Analysis is undertaken by modelling life as a novel statistico-deterministic version of a Turing machine, i.e. as a series of transitions between states at successive instants of time. Using this model it is proven by induction that the entire course of life is independent of the action of free will. Although determined by prior state, the probability of transitions between states in response to a standard environmental stimulus is not equal to 1 and the transitions may differ quantitatively at the molecular level and qualitatively at the level of the whole organism. Transitions between states correspond to behaviours. It is shown that the behaviour of identical twins (or clones), although determined, would be incompletely predictable and non-identical, creating an illusion of the operation of 'free will'. 'Free will' is a convenient construct for current judicial systems and social control because it allows rationalization of punishment for those whose behaviour falls outside socially defined norms. Indeed, it is conceivable that maintenance of ideas of free will has co-evolved with community morality to reinforce its operation. If the concept is free will is to be maintained it would require revision of our current physical theories.

Assessing flow in physical activity: The Flow State Scale-2 and Dispositional Flow Scale-2

The Flow State Scale-2 (FSS-2) and Dispositional Flow Scale-2 (DFS-2) are presented as two self-report instruments designed to assess flow experiences in physical activity. Item modifications were made to the original versions of these scales in order to improve the measurement of some of the flow dimensions. Confirmatory factor analyses of an item identification and a cross-validation sample demonstrated a good fit of the new scales. There was support for both a 9-first-order factor model and a higher order model with a global flow factor. The item identification sample yielded mean item loadings on the first-order factor of .78 for the FSS-2 and .77 for the DFS-2. Reliability estimates ranged from .80 to .90 for the FSS-2, and .81 to .90 for the DFS-2. In the cross-validation sample, mean item loadings on the first-order factor were .80 for the FSS-2, and .73 for the DFS-2. Reliability estimates ranged between .80 to .92 for the FSS-2 and .78 to .86 for the DFS-2. The scales are presented as ways of assessing flow experienced within a particular event (FSS-2) or the frequency of flow experiences in chosen physical activity in general (DFS-2).

Review of Contact and Dynamic Phenomena in Cold Roll Forming

This review reflects the state of the art in study of contact and dynamic phenomena occurring in cold roll forming. The importance of taking these phenomena into account is determined by significant machine time and tooling costs spent on worn out forming rolls replacement and equipment adjustment in cold roll forming. Predictive modelling of the tool wear caused by contact and dynamic phenomena can reduce the production losses in this technological process.

Religious Information Poverty in Australian State Schools

This paper introduces the concept of religious information poverty in Australian state schools from an information science perspective. Information scientists have been theorising about the global information society for some time, along with its increased provision of vital information for the good of the world. Australian state schools see themselves as preparing children for effective participation in the information society, yet Australian children are currently suffering a religious illiteracy that undermines this goal. Some reasons and theories are offered to explain the existence of religious information poverty in state schools, and suggestions for professional stakeholders are offered for its alleviation.