How robust is a healthcare system? How does a patient navigate the system and what is the cost (e.g., number of medical services required or number of times the medical provider had to be changed to get access to the required medical services) incurred from the first symptoms to getting cured? How will it fare in the wake to a sudden epidemic or a disaster? How are all of these affected by administrative decisions such as allocating/diminishing resources in various areas or centralising services? These are the questions motivating our study on a formal prototype model for a healthcare system. We propose that a healthcare system can be understood as a distributed system with independent nodes (healthcare providers) computing according to their own resources and constraints, with tasks (patient needs) being allocated between the nodes. The questions about the healthcare system become in this context questions about resource availability and distribution between the nodes. We construct in this paper an Event-B model capturing the basic functionality of a simplified healthcare system: patients with different types of medical needs being allocated to suitable medical providers, and navigating between different providers for their turn for multi-step treatments.

In this paper we present a stepwise formal development of the Optimised Link State Routing (OLSR) protocol in Event-B. OLSR is a proactive routing protocol which finds routes for different destinations in advance by exchanging control messages through the network. As a consequence, whenever a data packet is injected into the network can be delivered to a certain destination immediately. To achieve this, routing tables in OLSR are continuously updated, by following a rather complicated algorithm. By modelling OLSR in Event-B, we address the scalability problem of our previous work [1], and structure the OLSR complexity in five distinct abstraction layers. These layers are manageable to understand and to verify and are linked to each other by refinement. As Event-B is supported by a theorem proving platform (Rodin), we model and prove functional properties of OLSR in an automated and interactive manner, at a highly general level. Our approach can serve as a proof-of-concept to be adapted to modelling and verifying of the other routing protocols for large-scale networks.

The Optimised Link State Routing (OLSR) protocol is a proactive, ad-hoc distributed routing protocol for Wireless Mesh Networks (WMNs). In this paper we demonstrate that by introducing a new type of message for this protocol (namely an ERROR message), the recovery time for routing in the presence of random link failures decreases. We illustrate our findings via formal model checking experiments in Uppaal. Decreased recovery time is essential for, e.g., emergency response networks and other critical WMNs.

A routing protocol disseminates information for route selection between any two nodes on a network and thus provides the ground for sending data (packets) through the network. Routing protocols are used in a wide range of application areas in various types of networks, such as Local Area Networks (LAN), Mobile Ad hoc Networks (MANETs) or Wireless Mesh Networks (WMN). Due to the application diversity, different protocols have been developed. For instance in the case of WMNs, there are reactive protocols, such as AODV, and proactive protocols, such as OLSR. These protocols have been already implemented and deployed. However, it is unclear which protocol should be used in certain circumstances: Could we assume that AODV performs better than OLSR in case of reduced network traffic? Is OLSR better than AODV when considering mobile networks? To answer these questions systematically, we aim at formally defining properties that can be used as metrics (measurements) for routing protocols. To evaluate the measurements, we focus on comparing AODV and OLSR protocols.

No abstract available.

editorial Free AccessKaisa Sere: In Memoriam Authors: Luigia Petre Department of Information Technologies, Åbo Akademi University, Joukahaisenkatu 3-5A, 20520, Turku, Finland Department of Information Technologies, Åbo Akademi University, Joukahaisenkatu 3-5A, 20520, Turku, FinlandSearch about this author , Elena Troubitsyna Department of Information Technologies, Åbo Akademi University, Joukahaisenkatu 3-5A, 20520, Turku, Finland Department of Information Technologies, Åbo Akademi University, Joukahaisenkatu 3-5A, 20520, Turku, FinlandSearch about this author , Marina Waldén Department of Information Technologies, Åbo Akademi University, Joukahaisenkatu 3-5A, 20520, Turku, Finland Department of Information Technologies, Åbo Akademi University, Joukahaisenkatu 3-5A, 20520, Turku, FinlandSearch about this author Authors Info & Claims Formal Aspects of ComputingVolume 26Issue 2Mar 2014 pp 197–201https://doi.org/10.1007/s00165-013-0292-5Published:01 March 2014Publication History 0citation11DownloadsMetricsTotal Citations0Total Downloads11Last 12 Months9Last 6 weeks1 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

Wireless sensor–actor networks are a recent development of wireless networks where both ordinary sensor nodes and more sophisticated and powerful nodes, called actors, are present. In this paper we introduce several, increasingly more detailed, formal models for this type of wireless networks. These models formalise a recently introduced algorithm for recovering actor–actor coordination links via the existing sensor infrastructure. We prove via refinement that this recovery is correct and that it terminates in a finite number of steps. In addition, we propose a generalisation of our formal development strategy, which can be reused in the context of a wider class of networks. We elaborate our models within the Event-B formalism, while our proofs are carried out using the RODIN platform — an integrated development framework for Event-B.

A reliable approach to designing systems is by applying formal methods, based on logics and set theory. In formal methods refinement based, we develop the system models stepwise, from an abstract level to a concrete one by gradually adding details. Each detail-adding level is proved to still validate the properties of the more abstract level. Due to the high complexity and the high reliability requirements of 3D NoCs, formal methods provide promising solutions for modeling and verifying their communication schemes. In this paper, we present a general model for specifying the 3D NoC multicast communication scheme. We then refine our model to two communication schemes, : unicast and multicast, via the XYZ routing algorithm in order to put forward the correct-by-construction concrete models.