An automated failure mode and effect analysis based on high-level design specificication with behavior trees

Formal methods have significant benefits for developing safety critical systems, in that they allow for correctness proofs, model checking safety and liveness properties, deadlock checking, etc. However, formal methods do not scale very well and demand specialist skills, when developing real-world systems. For these reasons, development and analysis of large-scale safety critical systems will require effective integration of formal and informal methods. In this paper, we use such an integrative approach to automate Failure Modes and Effects Analysis (FMEA), a widely used system safety analysis technique, using a high-level graphical modelling notation (Behavior Trees) and model checking. We inject component failure modes into the Behavior Trees and translate the resulting Behavior Trees to SAL code. This enables us to model check if the system in the presence of these faults satisfies its safety properties, specified by temporal logic formulas. The benefit of this process is tool support that automates the tedious and error-prone aspects of FMEA.

Fossil trees in ancient fluvial channel deposits: evidence of seasonal and longer-term climatic variability

It has been established that large numbers of certain trees can survive in the beds of rivers of northeastern Australia where a strongly seasonal distribution of precipitation causes extreme variations in flow on both a yearly and longer-term basis. In these rivers, minimal flow occurs throughout much of any year and for periods of up to several years, allowing the trees to become established and to adapt their form in order to facilitate their survival in environments that experience periodic inundation by fast-flowing, debris-laden water. Such trees (notably paperbark trees of the angiosperm genus Melaleuca) adopt a reclined to prostrate, downstream-trailing habit, have a multiple-stemmed form, modified crown with weeping foliage, development of thick, spongy bark, anchoring of roots into firm to lithified substrates beneath the channel floor, root regeneration, and develop in flow-parallel, linear groves. Individuals from within flow-parallel, linear groves are preserved in situ within the alluvial deposit of the river following burial and death. Four examples of in situ tree fossils within alluvial channel deposits in the Permian of eastern Australia demonstrate that specialised riverbed plant communities also existed at times in the geological past. These examples, from the Lower Permian Carmila Beds, Upper Permian Moranbah Coal Measures and Baralaba Coal Measures of central Queensland and the Upper Permian Newcastle Coal Measures of central New South Wales, show several of the characteristics of trees described from modern rivers in northeastern Australia, including preservation in closely-spaced groups. These properties, together with independent sedimentological evidence, suggest that the Permian trees were adapted to an environment affected by highly variable runoff, albeit in a more temperate climatic situation than the modem Australian examples. It is proposed that occurrences of fossil trees preserved in situ within alluvial channel deposits may be diagnostic of environments controlled by seasonal and longer-term variability in fluvial runoff, and hence may have value in interpreting aspects of palaeoclimate from ancient alluvial successions. (C) 2001 Elsevier Science B.V. All rights reserved.