Modelling the control strategies against dengue in Singapore

Notified cases of dengue infections in Singapore reached historical highs in 2004 (9459 cases) and 2005 (13 817 cases) and the reason for such all increase is still to be established. We apply a mathematical model for dengue infection that takes into account the seasonal variation in incidence, characteristic of dengue fever, and which mimics the 2004-2005 epidemics in Singapore. We simulated a set of possible control strategies and confirmed the intuitive belief that killing adult mosquitoes is the most effective strategy to control an ongoing epidemic. On the other hand, the control of immature forms was very efficient ill preventing the resurgence of dengue epidemics. Since the control of immature forms allows the reduction of adulticide, it seems that the best strategy is to combine both adulticide and larvicide control measures during an outbreak, followed by the maintenance of larvicide methods after the epidemic has subsided. In addition, the model showed that the mixed strategy of adulticide and larvicide methods introduced by the government seems to be very effective in reducing the number of cases in the first weeks after the start of control.

Concurreny based transition refinement for the verification of distributed algorithms

We suggest a new notion of behaviour preserving transition refinement based on partial order semantics. This notion is called transition refinement. We introduced transition refinement for elementary (low-level) Petri Nets earlier. For modelling and verifying complex distributed algorithms, high-level (Algebraic) Petri nets are usually used. In this paper, we define transition refinement for Algebraic Petri Nets. This notion is more powerful than transition refinement for elementary Petri nets because it corresponds to the simultaneous refinement of several transitions in an elementary Petri net. Transition refinement is particularly suitable for refinement steps that increase the degree of distribution of an algorithm, e.g. when synchronous communication is replaced by asynchronous message passing. We study how to prove that a replacement of a transition is a transition refinement.

Behavioral Types for Embedded Software - A Survey

At present, there is a variety of formalisms for modeling and analyzing the communication behavior of components. Due to a tremendous increase in size and complexity of embedded systems accompanied by shorter time to market cycles and cost reduction, so called behavioral type systems become more and more important. This chapter presents an overview and a taxonomy of behavioral types. The intentions of this taxonomy are to provide a guidance for software engineers and to form the basis for future research.

Specification and Evaluation of Safety Properties in a Component-Based Software Engineering Process

Over the past years, component-based software engineering has become an established paradigm in the area of complex software intensive systems. However, many techniques for analyzing these systems for critical properties currently do not make use of the component orientation. In particular, safety analysis of component-based systems is an open field of research. In this chapter we investigate the problems arising and define a set of requirements that apply when adapting the analysis of safety properties to a component-based software engineering process. Based on these requirements some important component-oriented safety evaluation approaches are examined and compared.