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.

A simulation model of cereal-legume intercropping systems for semi-arid regions I. Model development

Cereal-legume intercropping plays an important role in subsistence food production in developing countries, especially in situations of limited water resources. Crop simulation can be used to assess risk for intercrop productivity over time and space. In this study, a simple model for intercropping was developed for cereal and legume growth and yield, under semi-arid conditions. The model is based on radiation interception and use, and incorporates a water stress factor. Total dry matter and yield are functions of photosynthetically active radiation (PAR), the fraction of radiation intercepted and radiation use efficiency (RUE). One of two PAR sub-models was used to estimate PAR from solar radiation; either PAR is 50% of solar radiation or the ratio of PAR to solar radiation (PAR/SR) is a function of the clearness index (K-T). The fraction of radiation intercepted was calculated either based on Beer's Law with crop extinction coefficients (K) from field experiments or from previous reports. RUE was calculated as a function of available soil water to a depth of 900 mm (ASW). Either the soil water balance method or the decay curve approach was used to determine ASW. Thus, two alternatives for each of three factors, i.e., PAR/SR, K and ASW, were considered, giving eight possible models (2 methods x 3 factors). The model calibration and validation were carried out with maize-bean intercropping systems using data collected in a semi-arid region (Bloemfontein, Free State, South Africa) during seven growing seasons (1996/1997-2002/2003). The combination of PAR estimated from the clearness index, a crop extinction coefficient from the field experiment and the decay curve model gave the most reasonable and acceptable result. The intercrop model developed in this study is simple, so this modelling approach can be employed to develop other cereal-legume intercrop models for semi-arid regions. (c) 2004 Elsevier B.V. All rights reserved.

Model-Driven safety evaluation with state-event-based component failure annotations

Over the past years, the paradigm of component-based software engineering has been established in the construction of complex mission-critical systems. Due to this trend, there is a practical need for techniques that evaluate critical properties (such as safety, reliability, availability or performance) of these systems. In this paper, we review several high-level techniques for the evaluation of safety properties for component-based systems and we propose a new evaluation model (State Event Fault Trees) that extends safety analysis towards a lower abstraction level. This model possesses a state-event semantics and strong encapsulation, which is especially useful for the evaluation of component-based software systems. Finally, we compare the techniques and give suggestions for their combined usage

Epidermal iontophoresis: I. Development of the ionic mobility-pore model

Purpose, An integrated ionic mobility-pore model for epidermal iontophoresis is developed from theoretical considerations using both the free volume and pore restriction forms of the model for a range of solute radii (r(j)) approaching the pore radii (r(p)) as well as approximation of the pore restriction form for r(j)/r(p) < 0.4. In this model, we defined the determinants for iontophoresis as solute size (defined by MV, MW or radius), solute mobility, solute shape, solute charge, the Debye layer thickness, total current applied, solute concentration, fraction ionized, presence of extraneous ions (defined by solvent conductivity), epidermal permselectivity, partitioning rates to account for interaction of unionized and ionized lipophilic solutes with the wall of the pore and electroosmosis. Methods, The ionic mobility-pore model was developed from theoretical considerations to include each of the determinants of iontophoretic transport. The model was then used to reexamine iontophoretic flux conductivity and iontophoretic flux-fraction ionized literature data on the determinants of iontophoretic flux. Results. The ionic mobility-pore model was found to be consistent with existing experimental data and determinants defining iontophoretic transport. However, the predicted effects of solute size on iontophoresis are more consistent with the pore-restriction than free volume form of the model. A reanalysis of iontophoretic flux-conductivity data confirmed the model's prediction that, in the absence of significant electroosmosis, the reciprocal of flux is linearly related to either donor or receptor solution conductivity. Significant interaction with the pore walls, as described by the model, accounted for the reported pH dependence of the iontophoretic transport for a range of ionizable solutes. Conclusions. The ionic mobility-pore iontophoretic model developed enables a range of determinants of iontophoresis to be described in a single unifying equation which recognises a range of determinants of iontophoretic flux.

API documentation with executable examples

The rise of component-based software development has created an urgent need for effective application program interface (API) documentation. Experience has shown that it is hard to create precise and readable documentation. Prose documentation can provide a good overview but lacks precision. Formal methods offer precision but the resulting documentation is expensive to develop. Worse, few developers have the skill or inclination to read formal documentation. We present a pragmatic solution to the problem of API documentation. We augment the prose documentation with executable test cases, including expected outputs, and use the prose plus the test cases as the documentation. With appropriate tool support, the test cases are easy to develop and read. Such test cases constitute a completely formal, albeit partial, specification of input/output behavior. Equally important, consistency between code and documentation is demonstrated by running the test cases. This approach provides an attractive bridge between formal and informal documentation. We also present a tool that supports compact and readable test cases; and generation of test drivers and documentation, and illustrate the approach with detailed case studies. (C) 2002 Elsevier Science Inc. All rights reserved.

Structural refinement of systems specified in object-z and CSP

This paper is concerned with methods for refinement of specifications written using a combination of Object-Z and CSP. Such a combination has proved to be a suitable vehicle for specifying complex systems which involve state and behaviour, and several proposals exist for integrating these two languages. The basis of the integration in this paper is a semantics of Object-Z classes identical to CSP processes. This allows classes specified in Object-Z to be combined using CSP operators. It has been shown that this semantic model allows state-based refinement relations to be used on the Object-Z components in an integrated Object-Z/CSP specification. However, the current refinement methodology does not allow the structure of a specification to be changed in a refinement, whereas a full methodology would, for example, allow concurrency to be introduced during the development life-cycle. In this paper, we tackle these concerns and discuss refinements of specifications written using Object-Z and CSP where we change the structure of the specification when performing the refinement. In particular, we develop a set of structural simulation rules which allow single components to be refined to more complex specifications involving CSP operators. The soundness of these rules is verified against the common semantic model and they are illustrated via a number of examples.

Development of a dosage strategy in patients receiving enoxaparin by continuous intravenous infusion using modelling and simulation

Aim To develop an appropriate dosing strategy for continuous intravenous infusions (CII) of enoxaparin by minimizing the percentage of steady-state anti-Xa concentration (C-ss) outside the therapeutic range of 0.5-1.2 IU ml(-1). Methods A nonlinear mixed effects model was developed with NONMEM (R) for 48 adult patients who received CII of enoxaparin with infusion durations that ranged from 8 to 894 h at rates between 100 and 1600 IU h(-1). Three hundred and sixty-three anti-Xa concentration measurements were available from patients who received CII. These were combined with 309 anti-Xa concentrations from 35 patients who received subcutaneous enoxaparin. The effects of age, body size, height, sex, creatinine clearance (CrCL) and patient location [intensive care unit (ICU) or general medical unit] on pharmacokinetic (PK) parameters were evaluated. Monte Carlo simulations were used to (i) evaluate covariate effects on C-ss and (ii) compare the impact of different infusion rates on predicted C-ss. The best dose was selected based on the highest probability that the C-ss achieved would lie within the therapeutic range. Results A two-compartment linear model with additive and proportional residual error for general medical unit patients and only a proportional error for patients in ICU provided the best description of the data. Both CrCL and weight were found to affect significantly clearance and volume of distribution of the central compartment, respectively. Simulations suggested that the best doses for patients in the ICU setting were 50 IU kg(-1) per 12 h (4.2 IU kg(-1) h(-1)) if CrCL < 30 ml min(-1); 60 IU kg(-1) per 12 h (5.0 IU kg(-1) h(-1)) if CrCL was 30-50 ml min(-1); and 70 IU kg(-1) per 12 h (5.8 IU kg(-1) h(-1)) if CrCL > 50 ml min(-1). The best doses for patients in the general medical unit were 60 IU kg(-1) per 12 h (5.0 IU kg(-1) h(-1)) if CrCL < 30 ml min(-1); 70 IU kg(-1) per 12 h (5.8 IU kg(-1) h(-1)) if CrCL was 30-50 ml min(-1); and 100 IU kg(-1) per 12 h (8.3 IU kg(-1) h(-1)) if CrCL > 50 ml min(-1). These best doses were selected based on providing the lowest equal probability of either being above or below the therapeutic range and the highest probability that the C-ss achieved would lie within the therapeutic range. Conclusion The dose of enoxaparin should be individualized to the patients' renal function and weight. There is some evidence to support slightly lower doses of CII enoxaparin in patients in the ICU setting.

Integrating formal specification and software verification and validation

It is not surprising that students are unconvinced about the benefits of formal methods if we do not show them how these methods can be integrated with other activities in the software lifecycle. In this paper, we describe an approach to integrating formal specification with more traditional verification and validation techniques in a course that teaches formal specification and specification-based testing. This is accomplished through a series of assignments on a single software component that involves specifying the component in Object-Z, validating that specification using inspection and a specification animation tool, and then testing an implementation of the specification using test cases derived from the formal specification.

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.

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.

Proceedings Ninth Asia-Pacific Software Engineering Conference. ASPEC 2002

The following topics are dealt with: Requirements engineering; components; design; formal specification analysis; education; model checking; human computer interaction; software design and architecture; formal methods and components; software maintenance; software process; formal methods and design; server-based applications; review and testing; measurement; documentation; management and knowledge-based approaches.

Assessing the competitiveness of loss allocation methods in a deregulated electricity market

This paper critically assesses several loss allocation methods based on the type of competition each method promotes. This understanding assists in determining which method will promote more efficient network operations when implemented in deregulated electricity industries. The methods addressed in this paper include the pro rata [1], proportional sharing [2], loss formula [3], incremental [4], and a new method proposed by the authors of this paper, which is loop-based [5]. These methods are tested on a modified Nordic 32-bus network, where different case studies of different operating points are investigated. The varying results obtained for each allocation method at different operating points make it possible to distinguish methods that promote unhealthy competition from those that encourage better system operation.

A framework of lessons learned from community-based marine reserves and its effectiveness in guiding a new coastal management initiative in the Philippines

Community-based coastal resource management has been widely applied within the Philippines. However, small-scale community-based reserves are often inefficient owing to management inadequacies arising because of a lack of local support or enforcement or poor design. Because there are many potential pitfalls during the establishment of even small community-based reserves, it is important for coastal managers, communities, and facilitating institutions to have access to a summary of the key factors for success. Reviewing relevant literature, we present a framework of lessons learned during the establishment of protected areas, mainly in the Philippines. The framework contains summary guidance on the importance of (1) an island location, (2) small community population size, (3) minimal effect of land-based development, (4) application of a bottom-up approach, (5) an external facilitating institution, (6) acquisition of title, (7) use of a scientific information database, (8) stakeholder involvement, (9) the establishment of legislation, (10) community empowerment, (11) alternative livelihood schemes, (12) surveillance, (13) tangible management results, (14) continued involvement of external groups after reserve establishment, and (15) small-scale project expansion. These framework components guided the establishment of a community-based protected area at Danjugan Island, Negros Occidental, Philippines. This case study showed that the framework was a useful guide that led to establishing and implementing a community-based marine reserve. Evaluation of the reserve using standard criteria developed for the Philippines shows that the Danjugan Island protected area can be considered successful and sustainable. At Danjugan Island, all of the lessons synthesized in the framework were important and should be considered elsewhere, even for relatively small projects. As shown in previous projects in the Philippines, local involvement and stewardship of the protected area appeared particularly important for its successful implementation. The involvement of external organizations also seemed to have a key role in the success of the Danjugan Island project by guiding local decision-makers in the sociobiological principles of establishing protected areas. However, the relative importance of each component of the framework will vary between coastal management initiatives both within the Philippines and across the wider Asian region.

Type III secretion contact-dependent model for the intracellular development of Chlamydia

The medically significant genus Chlamydia is a class of obligate intracellular bacterial pathogens that replicate within vacuoles in host eukaryotic cells termed inclusions. Chlamydia's developmental cycle involves two forms; an infectious extracellular form, known as an elementary body (EB), and a non-infectious form, known as the reticulate body (RB), that replicates inside the vacuoles of the host cells. The RB surface is covered in projections that are in intimate contact with the inclusion membrane. Late in the developmental cycle, these reticulate bodies differentiate into the elementary body form. In this paper, we present a hypothesis for the modulation of these developmental events involving the contact-dependent type III secretion (TTS) system. TTS surface projections mediate intimate contact between the RB and the inclusion membrane. Below a certain number of projections, detachment of the RB provides a signal for late differentiation of RB into EB. We use data and develop a mathematical model investigating this hypothesis. If the hypothesis proves to be accurate, then we have shown that increasing the number of inclusions per host cell will increase the number of infectious progeny EB until some optimal number of inclusions. For more inclusions than this optimum, the infectious yield is reduced because of spatial restrictions. We also predict that a reduction in the number of projections on the surface of the RB (and as early as possible during development) will significantly reduce the burst size of infectious EB particles. Many of the results predicted by the model can be tested experimentally and may lead to the identification of potential targets for drug design. © Society for Mathematical Biology 2006.

Verifying data refinements using a model checker

In this paper, we consider how refinements between state-based specifications (e.g., written in Z) can be checked by use of a model checker. Specifically, we are interested in the verification of downward and upward simulations which are the standard approach to verifying refinements in state-based notations. We show how downward and upward simulations can be checked using existing temporal logic model checkers. In particular, we show how the branching time temporal logic CTL can be used to encode the standard simulation conditions. We do this for both a blocking, or guarded, interpretation of operations (often used when specifying reactive systems) as well as the more common non-blocking interpretation of operations used in many state-based specification languages (for modelling sequential systems). The approach is general enough to use with any state-based specification language, and we illustrate how refinements between Z specifications can be checked using the SAL CTL model checker using a small example.