Procedures and parameters in the real-time program refinement calculus

The real-time refinement calculus is a formal method for the systematic derivation of real-time programs from real-time specifications in a style similar to the non-real-time refinement calculi of Back and Morgan. In this paper we extend the real-time refinement calculus with procedures and provide refinement rules for refining real-time specifications to procedure calls. A real-time specification can include constraints on, not only what outputs are produced, but also when they are produced. The derived programs can also include time constraints oil when certain points in the program must be reached; these are expressed in the form of deadline commands. Such programs are machine independent. An important consequence of the approach taken is that, not only are the specifications machine independent, but the whole refinement process is machine independent. To implement the machine independent code on a target machine one has a separate task of showing that the compiled machine code will reach all its deadlines before they expire. For real-time programs, externally observable input and output variables are essential. These differ from local variables in that their values are observable over the duration of the execution of the program. Hence procedures require input and output parameter mechanisms that are references to the actual parameters so that changes to external inputs are observable within the procedure and changes to output parameters are externally observable. In addition, we allow value and result parameters. These may be auxiliary parameters, which are used for reasoning about the correctness of real-time programs as well as in the expression of timing deadlines, but do not lead to any code being generated for them by a compiler. (c) 2006 Elsevier B.V. All rights reserved.

The importance of forest area and configuration relative to local habitat factors for conserving forest mammals: A case study of koalas in Queensland, Australia

The loss and fragmentation of forest habitats by human land use are recognised as important factors influencing the decline of forest-dependent fauna. Mammal species that are dependent upon forest habitats are particularly sensitive to habitat loss and fragmentation because they have highly specific habitat requirements, and in many cases have limited ability to move through and utilise the land use matrix. We addressed this problem using a case study of the koala (Phascolarctos cinereus) surveyed in a fragmented rural-urban landscape in southeast Queensland, Australia. We applied a logistic modelling and hierarchical partitioning analysis to determine the importance of forest area and its configuration relative to site (local) and patch-level habitat variables. After taking into account spatial auto-correlation and the year of survey, we found koala occurrence increased with the area of all forest habitats, habitat patch size and the proportion of primary Eucalyptus tree species; and decreased with mean nearest neighbour distance between forest patches, the density of forest patches, and the density of sealed roads. The difference between the effect of habitat area and configuration was not as strong as theory predicts, with the configuration of remnant forest becoming increasingly important as the area of forest habitat declines. We conclude that the area of forest, its configuration across the landscape, as well as the land use matrix, are important determinants of koala occurrence, and that habitat configuration should not be overlooked in the conservation of forest-dependent mammals, such as the koala. We highlight the implications of these findings for koala conservation. (c) 2006 Elsevier Ltd. All rights reserved.