Synchronous coordination systems allow the exchange of data by logically indivisible actions involving all coordinated entities. This paper introduces behavioural automata, a logically synchronous coordination model based on the Reo coordination language, which focuses on relevant aspects for the concurrent evolution of these systems. We show how our automata model encodes the Reo and Linda coordination models and how it introduces an explicit predicate that captures the concurrent evolution, distinguishing local from global actions, and lifting the need of most synchronous models to involve all entities at each coordination step, paving the way to more scalable implementations.
Este artigo propõe a criação de uma arquitetura que permita ao utilizador efetuar uma gestão dos seus dispositivos de comunicação por forma a aceder aos serviços contratados e proporcionar a mobilidade de sessão e identidade. Neste sentido foi desenvolvida uma arquitetura que oferece ao utilizador uma visão unificada de todos os seus dispositivos de comunicação e assim, disponibilizar uma forma simples e inovadora de gerir os dispositivos e a informação pessoal de cada utilizador. Esta
arquitetura proporciona a mobilidade de terminal, bem como a mobilidade de identidade no mesmo dispositivo e entre dispositivos diferentes, oferecendo assim uma utilização mais eficiente dos recursos disponíveis. Com o propósito de testar a arquitetura elaborada, foram efetuados testes funcionais que demonstram que as especificações inicialmente propostas foram cumpridas. Com base nos testes efetuados, foi realizada uma avaliação do impacto no utilizador que a arquitetura induz, concluindo-se que esta solução é uma mais valia para o utilizador, tanto nas funcionalidades como na usabilidade.
We report on a case study investigating current practice in the use of a programmable infusion pump. We start by formalising an existing description of the procedure followed by nurses for setting up a commercial infusion pump obtained via observation and interview. We then compare and contrast this procedure with a formal description of the sequence of actions reported in the pump's user manual. Mismatches were validated by a training manager. The aim of this comparison is to point out how minor mismatches between the two descriptions can be used to reveal major safety issues. Our contributions are: first, we analyse a real-world system and show the importance of having a clear and consistent specification of the procedures; second, we show how a graph-based notation can be conveniently used for building non-ambiguous and intuitive specifications. We argue that this can provide support to an investigator when building a description of actual practice in that it can help focus attention on areas to observe more closely and questions to ask to understand why procedures, as followed, are the way they are.
Cauchi A, Curzon P, Eslambolchilar P, Gimblett A, Huang H, Lee P, Li Y, Masci P, Oladimeji P, Ruksenas R et al..
2011. Towards Dependable Number Entry for Medical Devices. Eics4Med, the 1st International Workshop on Engineering Interactive Computing Systems for Medicine and Health Care. CEUR Workshop Proceedings, vol 727 Abstract
Number entry is an ubiquitous task in medical devices, but is implemented in many different ways, from decimal keypads to seemingly simple up/down buttons. Operator manuals often do not give clear and complete explanations, and all approaches have subtle variations, with details varying from device to device. This paper explores the design issues, critiques designs, and shows that methods have advantages and disadvantages, particularly in terms of undetected error rates.
We define the predictability of a user interface as the property that an idealised user can predict with sufficient certainty the effect of any action in a given state in a system, where state information is inferred from the perceptible output of the system. In our definition, the user is not required to have full knowledge of a history of actions from an initial state to the current state. Typically such definitions rely on cognitive and knowledge assumptions; in this paper we explore the notion in the situation where the user is an idealised expert and understands perfectly how the device works. In this situation predictability concerns whether the user can tell what state the device is in and accurately predict the consequences of an action from that state simply by looking at the device; normal human users can certainly do no better. We give a formal definition of predictability in higher order logic and explore how real systems can be verified against the property. We specify two real number entry interfaces in the healthcare domain (drug infusion pumps) as case studies of predictable and unpredictable user interfaces. We analyse the specifications with respect to our formal definition of predictability and thus show how to make unpredictable systems predictable.
Dynamic environments may include autonomous and decentralised components that pose many challenges from the point of view of interoperability, thus triggering research studies in several directions. One recent research direction explores the automatic composition of heterogeneous systems through connectors synthesised at run-time. Besides functional properties, such connectors generally need to satisfy also non-functional (dependability-related) properties. This paper investigates the definition of an automated procedure to support the synthesis of dependable connectors.
Model-based analysis is a well-established method to assess the dependability of a system before deployment. It is well known that, in highly dynamic contexts, the accuracy of the analysis results can be limited because unpredictable phenomena may affect the system during its operation. In such contexts, the analysis typically needs to be refined with data obtained from real system executions. In this paper we tackle the issue of refining model-based dependability analysis in automated systems through monitoring. Specifically, we report on our preliminary results on the development of a system that exploits the synergic use of an automated approach for model-based dependability analysis and a flexible monitoring architecture.
It is well known that systems built with resilient components are not necessarily resilient systems. Nevertheless, when studying the resilience of work systems characterised by continuous inter-operations among humans and devices, analysts generally concentrate only on localised interactions among humans and devices. Consequently they fail to capture the distributed nature of the mechanisms that guide interactions in dynamic interactive systems. In this paper, as a result of work on the resilience of medical systems with respect to human error, we propose a framework for reasoning about the resilience of complex dynamic interactive systems. To do this we exploit concepts from three different areas: the automated synthesis of resilient systems, formal methods for user-centred design, and distributed cognition.
We propose a constructive procedure for building a distribut-ed cognition model of a system out of contextual / ethnographic data. We then show how such a model can be conveniently used for studying, in a repeatable and justifiable way, if a system correctly implements selected user-centred design principles. Our approach thus complements user studies in that it enables reasoning about the situated use of a teamwork system even before direct user involvement. We have applied our procedure to a healthcare case study. In particular, we have re-analysed a well-known adverse incident that led to a fatality and for which a comprehensive investigation report is in the public domain. By reasoning about the distributed cognition model, we identified several issues that were not addressed in the incident report nor in other subsequent analyses.
We present the specification of a basic library of dependability mechanisms that can be used within automated approaches for synthesising dependable connectors in heterogeneous networks. The library builds on classical dependability patterns, such as majority voting and retry, and uses the concept of overlay networks for triggering the synthesis of specific dependability mechanisms in the connector from high-level specifications. We translated such dependability mechanisms into SAN models with the aim to evaluate, through model-based analysis, which dependability mechanisms should be embedded in the synthesised connector for ensuring a given dependability level between networked systems willing to be connected. A case study is also presented to show the application of selected library mechanisms. This work is carried out in the context of connect, a European FET project which is investigating the possibility of enabling long-lasting inter-operation among networked systems by synthesising mediating connectors at run-time.
Parallel corpora are resources used in Natural Language Processing and Computational Linguistics. They are defined as a set of texts, in different languages, that are translations of each other. Note that these translations do not need to cover the full document, as we might have sentences translated just on some of the languages. When dealing with the process of sharing resources, recent years have bet on the use of XML formats. This is no different when talking about parallel corpora sharing. When visiting different projects in the web that release parallel corpora for download, we can find at least three different formats. In fact, this abundance of formats has led some projects to adopt all the three formats. This article discusses these three main formats: XML Corpus Encoding Standard, Translation Memory Exchange format and the Text Encoding Initiative. We will compare their formal definition and their XML schema.
Many errors in spreadsheet formulas can be avoided if spreadsheets are built automatically from higher-level models that can encode and enforce consistency constraints.
However, designing such models is time consuming and requires expertise beyond the knowledge to work with spreadsheets. Legacy spreadsheets pose a particular challenge to the approach of controlling spreadsheet evolution through higher-level models, because the need for a model might be overshadowed by two problems: (A) The benefit of creating a spreadsheet is lacking since the legacy spreadsheet already exists, and (B) existing data must be transferred into the new model-generated spreadsheet.To address these problems and to support the modeldriven spreadsheet engineering approach, we have developed a tool that can automatically infer ClassSheet models from spreadsheets. To this end, we have adapted a method to infer entity/relationship models from relational database to the spreadsheets/ClassSheets realm. We have implemented our techniques in the HAEXCEL framework and integrated it with the ViTSL/Gencel spreadsheet generator, which allows the automatic generation of refactored spreadsheets from the inferred ClassSheet model. The resulting spreadsheet guides further changes and provably safeguards the spreadsheet against a large class of formula errors. The developed tool is a significant contribution to spreadsheet (reverse) engineering, because it fills an important gap and allows a promising design method (ClassSheets) to be applied to a huge collection of legacy spreadsheets with minimal effort.