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.

Physiologically based synthetic models of hepatic disposition

Current Physiologically based pharmacokinetic (PBPK) models are inductive. We present an additional, different approach that is based on the synthetic rather than the inductive approach to modeling and simulation. It relies on object-oriented programming A model of the referent system in its experimental context is synthesized by assembling objects that represent components such as molecules, cells, aspects of tissue architecture, catheters, etc. The single pass perfused rat liver has been well described in evaluating hepatic drug pharmacokinetics (PK) and is the system on which we focus. In silico experiments begin with administration of objects representing actual compounds. Data are collected in a manner analogous to that in the referent PK experiments. The synthetic modeling method allows for recognition and representation of discrete event and discrete time processes, as well as heterogeneity in organization, function, and spatial effects. An application is developed for sucrose and antipyrine, administered separately and together PBPK modeling has made extensive progress in characterizing abstracted PK properties but this has also been its limitation. Now, other important questions and possible extensions emerge. How are these PK properties and the observed behaviors generated? The inherent heuristic limitations of traditional models have hindered getting meaningful, detailed answers to such questions. Synthetic models of the type described here are specifically intended to help answer such questions. Analogous to wet-lab experimental models, they retain their applicability even when broken apart into sub-components. Having and applying this new class of models along with traditional PK modeling methods is expected to increase the productivity of pharmaceutical research at all levels that make use of modeling and simulation.

Formalising behaviour trees with CSP

Behaviour Trees is a novel approach for requirements engineering. It advocates a graphical tree notation that is easy to use and to understand. Individual requirements axe modelled as single trees which later on are integrated into a model of the system as a whole. We develop a formal semantics for a subset of Behaviour Trees using CSP. This work, on one hand, provides tool support for Behaviour Trees. On the other hand, it builds a front-end to a subset of the CSP notation and gives CSP users a new modelling strategy which is well suited to the challenges of requirements engineering.

Agent-based distributed software verification

Despite decades of research, the takeup of formal methods for developing provably correct software in industry remains slow. One reason for this is the high cost of proof construction, an activity that, due to the complexity of the required proofs, is typically carried out using interactive theorem provers. In this paper we propose an agent-oriented architecture for interactive theorem proving with the aim of reducing the user interactions (and thus the cost) of constructing software verification proofs. We describe a prototype implementation of our architecture and discuss its application to a small, but non-trivial case study.

Deregulation, competition policy and intra-professional contests in medical education

This paper investigates how government policy directions embracing deregulation and market liberalism, together with significant pre-existing tensions within the Australian medical profession, produced ground breaking change in the funding and delivery of medical education for general practitioners. From an initial view between and within the medical profession, and government, about the goal of improving the standards of general practice education and training, segments of the general practice community, particularly those located in rural and remote settings, displayed increasingly vocal concerns about the approach and solutions proffered by the predominantly urban-influenced Royal Australian College of General Practitioners (RACGP). The extent of dissatisfaction culminated in the establishment of the Australian College of Rural and Remote Medicine (ACRRM) in 1997 and the development of an alternative curriculum for general practice. This paper focuses on two decades of changes in general practice training and how competition policy acted as a justificatory mechanism for putting general practice education out to competitive tender against a background of significant intra-professional conflict. The government's interest in increasing efficiency and deregulating the 'closed shop' practices of professions, as expressed through national competition policy, ultimately exposed the existing antagonisms within the profession to public view and allowed the government some influence on the sacred cow of professional training. Government policy has acted as a mechanism of resolution for long standing grievances of the rural GPs and propelled professional training towards an open competition model. The findings have implications for future research looking at the unanticipated outcomes of competition and internal markets.

Computer-aided programming using formally specificed design templates

This paper describes a formal component language, used to support automated component-based program development. The components, referred to as templates, are machine processable, meaning that appropriate tool support, such as retrieval support, can be developed. The templates are highly adaptable, meaning that they can be applied to a wide range of problems. Some of the main features of the language are described, including: higher-order parameters; state variable declarations; specification statements and conditionals; applicability conditions and theories; meta-level place holders; and abstract data structures.

A Z based approach to verifying security protocols

Security protocols preserve essential properties, such as confidentiality and authentication, of electronically transmitted data. However, such properties cannot be directly expressed or verified in contemporary formal methods. Via a detailed example, we describe the phases needed to formalise and verify the correctness of a security protocol in the state-oriented Z formalism.

An Investigation into the adoption and implementation of computer aided production management systems:using the Rogers model of adoption and implementation and a social constuctionist account of technology

The research investigates the processes of adoption and implementation, by organisations, of computer aided production management systems (CAPM). It is organised around two different theoretical perspectives. The first part is informed by the Rogers model of the diffusion, adoption and implementation of innovations, and the second part by a social constructionist approach to technology. Rogers' work is critically evaluated and a model of adoption and implementation is distilled from it and applied to a set of empirical case studies. In the light of the case study data, strengths and weaknesses of the model are identified. It is argued that the model is too rational and linear to provide an adequate explanation of adoption processes. It is useful for understanding processes of implementation but requires further development. The model is not able to adequately encompass complex computer based technologies. However, the idea of 'reinvention' is identified as Roger's key concept but it needs to be conceptually extended. Both Roger's model and definition of CAPM found in the literature from production engineering tend to treat CAPM in objectivist terms. The problems with this view are addressed through a review of the literature on the sociology of technology, and it is argued that a social constructionist approach offers a more useful framework for understanding CAPM, its nature, adoption, implementation, and use. CAPM it is argued, must be understood on terms of the ways in which it is constituted in discourse, as part of a 'struggle for meaning' on the part of academics, professional engineers, suppliers, and users.

Supporting English language teachers doing further degrees at a distance:a web based strategy researched

This thesis explores how the world-wide-web can be used to support English language teachers doing further studies at a distance. The future of education worldwide is moving towards a requirement that we, as teacher educators, use the latest web technology not as a gambit, but as a viable tool to improve learning. By examining the literature on knowledge, teacher education and web training, a model of teacher knowledge development, along with statements of advice for web developers based upon the model are developed. Next, the applicability and viability of both the model and statements of advice are examined by developing a teacher support site (bttp://www. philseflsupport. com) according to these principles. The data collected from one focus group of users from sixteen different countries, all studying on the same distance Masters programme, is then analysed in depth. The outcomes from the research are threefold: A functioning website that is averaging around 15, 000 hits a month provides a professional contribution. An expanded model of teacher knowledge development that is based upon five theoretical principles that reflect the ever-expanding cyclical nature of teacher learning provides an academic contribution. A series of six statements of advice for developers of teacher support sites. These statements are grounded in the theoretical principles behind the model of teacher knowledge development and incorporate nine keys to effective web facilitation. Taken together, they provide a forward-looking contribution to the praxis of web supported teacher education, and thus to the potential dissemination of the research presented here. The research has succeeded in reducing the proliferation of terminology in teacher knowledge into a succinct model of teacher knowledge development. The model may now be used to further our understanding of how teachers learn and develop as other research builds upon the individual study here. NB: Appendix 4 is only available only available for consultation at Aston University Library with prior arrangement.

Enhanced semantic access to formal software models

The success of the Semantic Web, as the next generation of Web technology, can have profound impact on the environment for formal software development. It allows both the software engineers and machines to understand the content of formal models and supports more effective software design in terms of understanding, sharing and reusing in a distributed manner. To realise the full potential of the Semantic Web in formal software development, effectively creating proper semantic metadata for formal software models and their related software artefacts is crucial. In this paper, a methodology with tool support is proposed to automatically derive ontological metadata from formal software models and semantically describe them.

A pre-post test evaluation of the impact of the PELICAN MDT-TME development programme on the working lives of colorectal cancer team members

Background - The PELICAN Multidisciplinary Team Total Mesorectal Excision (MDT-TME) Development Programme aimed to improve clinical outcomes for rectal cancer by educating colorectal cancer teams in precision surgery and related aspects of multidisciplinary care. The Programme reached almost all colorectal cancer teams across England. We took the opportunity to assess the impact of participating in this novel team-based Development Programme on the working lives of colorectal cancer team members. Methods - The impact of participating in the programme on team members' self-reported job stress, job satisfaction and team performance was assessed in a pre-post course study. 333/568 (59%) team members, from the 75 multidisciplinary teams who attended the final year of the Programme, completed questionnaires pre-course, and 6-8 weeks post-course. Results - Across all team members, the main sources of job satisfaction related to working in multidisciplinary teams; whilst feeling overloaded was the main source of job stress. Surgeons and clinical nurse specialists reported higher levels of job satisfaction than team members who do not provide direct patient care, whilst MDT coordinators reported the lowest levels of job satisfaction and job stress. Both job stress and satisfaction decreased after participating in the Programme for all team members. There was a small improvement in team performance. Conclusions - Participation in the Development Programme had a mixed impact on the working lives of team members in the immediate aftermath of attending. The decrease in team members' job stress may reflect the improved knowledge and skills conferred by the Programme. The decrease in job satisfaction may be the consequence of being unable to apply these skills immediately in clinical practice because of a lack of required infrastructure and/or equipment. In addition, whilst the Programme raised awareness of the challenges of teamworking, a greater focus on tackling these issues may have improved working lives further.

An Intelligent System for Investigations and Provision of Safety for Complex Constructions

Methodology of computer-aided investigation and provision of safety for complex constructions and a prototype of the intelligent applied system, which implements it, are considered. The methodology is determined by the model of the object under scrutiny, by the structure and functions of investigation of safety as well as by a set of research methods. The methods are based on the technologies of object-oriented databases, expert systems and on the mathematical modeling. The intelligent system’s prototype represents component software, which provides for support of decision making in the process of safety investigations and investigation of the cause of failure. Support of decision making is executed by analogy, by determined search for the precedents (cases) with respect to predicted (on the stage of design) and observed (on the stage of exploitation) parameters of the damage, destruction and malfunction of a complex hazardous construction.

Generalized Nets Model of an E-Learning System Software Architecture

The paper has been presented at the International Conference Pioneers of Bulgarian Mathematics, Dedicated to Nikola Obreshko ff and Lubomir Tschakaloff , Sofi a, July, 2006.

An automated tool for semantic accessing to formal software models

Many software engineers have found that it is difficult to understand, incorporate and use different formal models consistently in the process of software developments, especially for large and complex software systems. This is mainly due to the complex mathematical nature of the formal methods and the lack of tool support. It is highly desirable to have software models and their related software artefacts systematically connected and used collaboratively, rather than in isolation. The success of the Semantic Web, as the next generation of Web technology, can have profound impact on the environment for formal software development. It allows both the software engineers and machines to understand the content of formal models and supports more effective software design in terms of understanding, sharing and reusing in a distributed manner. To realise the full potential of the Semantic Web in formal software development, effectively creating proper semantic metadata for formal software models and their related software artefacts is crucial. This paper proposed a framework that allows users to interconnect the knowledge about formal software models and other related documents using the semantic technology. We first propose a methodology with tool support is proposed to automatically derive ontological metadata from formal software models and semantically describe them. We then develop a Semantic Web environment for representing and sharing formal Z/OZ models. A method with prototype tool is presented to enhance semantic query to software models and other artefacts. © 2014.