A formal framework for modelling and analysing mobile systems

This paper presents a formal framework for modelling and analysing mobile systems. The framework comprises a collection of models of the dominant design paradigms which are readily extended to incorporate details of particular technologies, i.e., programming languages and their run-time support, and applications. The modelling language is Object-Z, an extension of the well-known Z specification language with explicit support for object-oriented concepts. Its support for object orientation makes Object-Z particularly suited to our task. The system structuring techniques offered by object-orientation are well suited to modelling mobile systems. In addition, inheritance and polymorphism allow us to exploit commonalities in mobile systems by defining more complex models in terms of simpler ones.

Contrasting mutual sexual selection on homologous signal traits in Drosophila serrata

The nature of male mating preferences, and how they differ from female mating preferences in species with conventional sex roles, has received little attention in sexual selection studies. We estimated the form and strength of sexual selection as a consequence of male and female mating preferences in a laboratory-based population of Drosophila serrata. The differences between sexual selection on male and female signal traits (cuticular hydrocarbons [CHCs]) were evaluated within a formal framework of linear and nonlinear selection gradients. Females tended to exert linear sexual selection on male CHCs, whereas males preferred intermediate female CHC phenotypes leading to convex (stabilizing) selection gradients. Possible mechanisms determining the nonlinear nature of sexual selection on female CHCs are proposed.

A framework and tool support for the systematic testing of model-based specifications

Formal specifications can precisely and unambiguously define the required behavior of a software system or component. However, formal specifications are complex artifacts that need to be verified to ensure that they are consistent, complete, and validated against the requirements. Specification testing or animation tools exist to assist with this by allowing the specifier to interpret or execute the specification. However, currently little is known about how to do this effectively. This article presents a framework and tool support for the systematic testing of formal, model-based specifications. Several important generic properties that should be satisfied by model-based specifications are first identified. Following the idea of mutation analysis, we then use variants or mutants of the specification to check that these properties are satisfied. The framework also allows the specifier to test application-specific properties. All properties are tested for a range of states that are defined by the tester in the form of a testgraph, which is a directed graph that partially models the states and transitions of the specification being tested. Tool support is provided for the generation of the mutants, for automatically traversing the testgraph and executing the test cases, and for reporting any errors. The framework is demonstrated on a small specification and its application to three larger specifications is discussed. Experience indicates that the framework can be used effectively to test small to medium-sized specifications and that it can reveal a significant number of problems in these specifications.

Events in Indonesia: exploring the limits to formal tourism trends forecasting methods in complex crisis situations

The desire to know the future is as old as humanity. For the tourism industry the demand for accurate foretelling of the future course of events is a task that consumes considerable energy and is of great significance to investors. This paper examines the issue of forecasting by comparing forecasts of inbound tourism made prior to the political and economic crises that engulfed Indonesia from 1997 onwards with actual arrival figures. The paper finds that current methods of forecasting are not able to cope with unexpected crises and other disasters and that alternative methods need to be examined including scenarios, political risk and application of chaos theory. The paper outlines a framework for classifying shocks according to a scale of severity, probability, type of event, level of certainty and suggested forecasting tools for each scale of shock. (C) 2003 Elsevier Science Ltd. All rights reserved.

An MDA approach towards integrating formal and informal modeling languages

This paper shows how formal and informal modeling languages can be cooperatively used in the MDA framework, and how transformations between models in these languages can be achieved using an MDA development environment. The integrated approach also provides an effective V&V technique for the MDA.

A tool for a formal pattern modeling language

This paper presents a formal but practical approach for defining and using design patterns. Initially we formalize the concepts commonly used in defining design patterns using Object-Z. We also formalize consistency constraints that must be satisfied when a pattern is deployed in a design model. Then we implement the pattern modeling language and its consistency constraints using an existing modeling framework, EMF, and incorporate the implementation as plug-ins to the Eclipse modeling environment. While the language is defined formally in terms of Object-Z definitions, the language is implemented in a practical environment. Using the plug-ins, users can develop precise pattern descriptions without knowing the underlying formalism, and can use the tool to check the validity of the pattern descriptions and pattern usage in design models. In this work, formalism brings precision to the pattern language definition and its implementation brings practicability to our pattern-based modeling approach.

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.