Tank monitoring: a pAMN case study

The introduction of probabilistic behaviour into the B-method is a recent development. In addition to allowing probabilistic behaviour to be modelled, the relationship between expected values of the machine state can be expressed and verified. This paper explores the application of probabilistic B to a simple case study: tracking the volume of liquid held in a tank by measuring the flow of liquid into it. The flow can change as time progresses, and sensors are used to measure the flow with some degree of accuracy and reliability, modelled as non-deterministic and probabilistic behaviour respectively. At the specification level, the analysis is concerned with the expectation clause in the probabilistic B machine and its consistency with machine operations. At the refinement level, refinement and equivalence laws on probabilistic GSL are used to establish that a particular design of sensors delivers the required level of reliability.     

基于物联网的自助洗车系统设计与实现

针对传统洗车低效率、高消耗等问题,设计实现了一套基于物联网技术的新型自助洗车机系统。系统分为洗车机终端和云服务器端两个部分。洗车机终端以STM32F103VET6作为主控芯片,并利用霍尔流量传感器获取水流量,实现流量计费。GPRS-SIM868模块可实现与远程服务器的无线数据通信,并通过搭载各类传感器采集洗车机的状态数据。同时,云服务器端与洗车机终端建立UDP通信,实现对洗车机终端数据的获取,并通过以Tomcat作为Web服务器、MySQL为数据库建立B/S架构的数据管理系统。用户可以根据洗车机终端LCD显示屏提供的信息,自主选择支付方式、洗车模式以及计费模式。同时,后台管理人员可以通过网络及时了解自助洗车机的相关信息,对洗车机进行实时监控与管理。     

Formal verification of a pervasive messaging system

As ubiquitous computing becomes a reality, its applications are increasingly being used in business-critical, mission-critical and even in safety-critical, areas. Such systems must demonstrate an assured level of correctness. One approach to the exhaustive analysis of the behaviour of systems is formal verification, whereby each important requirement is logically assessed against all possible system behaviours. While formal verification is often used in safety analysis, it has rarely been used in the analysis of deployed pervasive applications. Without such formality it is difficult to establish that the system will exhibit the correct behaviours in response to its inputs and environment. In this paper, we show how model-checking techniques can be applied to analyse the probabilistic behaviour of pervasive systems. As a case study we apply this technique to an existing pervasive message-forwarding system, Scatterbox. Scatterbox incorporates many typical characteristics of pervasive systems, such as dependence on sensor reliability and dependence on context. We assess the dynamic temporal behaviour of the system, including the analysis of probabilistic elements, allowing us to verify formal requirements even in the presence of uncertainty in sensors. We also draw some tentative conclusions concerning the use of formal verification for pervasive computing in general.     

Extensions of design potential concept for reliability-based design optimization to nonsmooth and extreme cases

The reliability-based design optimization (RBDO) can be described by the design potential concept in a unified system space, where the probabilistic constraint is identified by the design potential surface of the reliability target that is obtained analytically from the first-order reliability method (FORM). This paper extends the design potential concept to treat nonsmooth probabilistic constraints and extreme case design in RBDO. In addition, refinement of the design potential surface, which yields better optimum design, can be obtained using more accurate second-order reliability method (SORM). By integrating performance probability analysis into the iterative design optimization process, the design potential concept leads to a very effective design potential method (DPM) for robust system parameter design. It can also be applied effectively to extreme case design (ECD) by directly representing a probabilistic constraint in terms of the system performance function. Received July 25, 2000     

A statistics-based sensor selection scheme for continuous probabilistic queries in sensor networks

A common approach to improve the reliability of query results based on error-prone sensors is to introduce redundant sensors. However, using multiple sensors to generate the value for a data item can be expensive, especially in wireless environments where continuous queries are executed. Moreover, some sensors may not be working properly and their readings need to be discarded. In this paper, we propose a statistical approach to decide which sensor nodes to be used to answer a query. In particular, we propose to solve the problem with the aid of continuous probabilistic query (CPQ), which is originally used to manage uncertain data and is associated with a probabilistic guarantee on the query result. Based on the historical data values from the sensor nodes, the query type, and the requirement on the query, we present methods to select an appropriate set of sensors and provide reliable answers for several common aggregate queries. Our statistics-based sensor node selection algorithm is demonstrated in a number of simulation experiments, which shows that a small number of sensor nodes can provide accurate and robust query results.     

错误流模型:硬件故障的软件传播建模与分析

无论是可靠性工程还是软件可靠性中的可靠性模型,都难以描述硬件故障在程序中的传播问题.首先建立了计算数据流模型,并以无穷存储机器的指令集为例,说明可以为任意程序建立计算数据流图.在计算数据流模型的基础上,进一步建立了错误流模型.把计算过程中的错误分成物理错误和传播错误两种,通过分析这两种错误的本质和传播规律,给出了6条有关错误传播的规则和2条独立定律.根据这些规则和定律,能够计算出在程序运行过程中,任意时刻在任意位置上出现错误的概率.最后以一个简单的无穷存储机器程序为例,简要地展示了错误流模型描述硬件故障在     

Method for flow measurement in microfluidic channels based on electrical impedance spectroscopy

We have developed and characterized two novel micro flow sensors based on measuring the electrical impedance of the interface between the flowing liquid and metallic electrodes embedded on the channel walls. These flow sensors are very simple to fabricate and use, are extremely compact and can easily be integrated into most microfluidic systems. One of these devices is a micropore with two tantalum/platinum electrodes on its edges; the other is a micro channel with two tantalum/platinum electrodes placed perpendicular to the channel on its walls. In both sensors the flow rate is measured via the electrical impedance between the two metallic electrodes, which is the impedance of two metal–liquid junctions in series. The dependency of the metal–liquid junction impedance on the flow rate of the liquid has been studied. The effects of different parameters on the sensor’s outputs and its noise behavior are investigated. Design guidelines are extracted and applied to achieve highly sensitive micro flow sensors with low noise.     

Robust semi-supervised mixture probabilistic principal component regression model development and application to soft sensors

Traditional data-based soft sensors are constructed with equal numbers of input and output data samples, meanwhile, these collected process data are assumed to be clean enough and no outliers are mixed. However, such assumptions are too strict in practice. On one hand, those easily collected input variables are sometimes corrupted with outliers. On the other hand, output variables, which also called quality variables, are usually difficult to obtain. These two problems make traditional soft sensors cumbersome. To deal with both issues, in this paper, the Student's t distributions are used during mixture probabilistic principal component regression modeling to tolerate outliers with regulated heavy tails. Furthermore, a semi-supervised mechanism is incorporated into traditional probabilistic regression so as to deal with the unbalanced modeling issue. For simulation, two case studies are provided to demonstrate robustness and reliability of the new method.     

Probabilistic contracts for component-based design

We define a framework of probabilistic contracts for constructing component-based embedded systems, based on the formalism of discrete-time Interactive Markov Chains. A contract specifies the assumptions a component makes on its context and the guarantees it provides. Probabilistic transitions represent allowed uncertainty in the component behavior, for instance, to model internal choice or reliability. Action transitions are used to model non-deterministic behavior and communication between components. An interaction model specifies how components interact with each other. We provide the ingredients for a component-based design flow, including (1) contract satisfaction and refinement, (2) parallel composition of contracts over disjoint, interacting components, and (3) conjunction of contracts describing different requirements over the same component. Compositional design is enabled by congruence of refinement.     

Logic programming,abduction and probability

Probabilistic Horn abduction is a simple framework to combine probabilistic and logical reasoning into a coherent practical framework. The numbers can be consistently interpreted probabilistically, and all of the rules can be interpreted logically. The relationship between probabilistic Horn abduction and logic programming is at two levels. At the first level probabilistic Horn abduction is an extension of pure Prolog, that is useful for diagnosis and other evidential reasoning tasks. At another level, current logic programming implementation techniques can be used to efficiently implement probabilistic Horn abduction. This forms the basis of an “anytime” algorithm for estimating arbitrary conditional probabilities. The focus of this paper is on the implementation.     

Components as coalgebras: The refinement dimension

This paper characterises refinement of state-based software components modelled as pointed coalgebras for some Set endofunctors. The proposed characterisation is parametric on a specification of the underlying behaviour model introduced as a strong monad. This provides a basis to reason about (and transform) state-based software designs. In particular, it is shown how refinement can be applied to the development of the inequational subset of a calculus of generic software components.     

基于嵌入式Web服务器的水情测报系统的设计

为了便于在远程能够监测到水情,设计了一种基于ARM处理器的嵌入式Web服务器。通过以太网对水位、降雨量、流速传感器等进行远程监测和数据集中处理,提高远端机器的安全可靠性。给出了硬件设计原理框图,阐述了嵌入式TCP/IP协议栈的体系结构和相关接口。用户可通过远程终端访问嵌入式Web服务器及时获得更新数据。整个系统在实际应用中,取得了比较满意的效果。     

Refinement of actions and equivalence notions for concurrent systems

We study an operator for refinement of actions to be used in the design of concurrent systems. Actions on a given level of abstraction are replaced by more complicated processes on a lower level. This is done in such a way that the behaviour of the refined system may be inferred compositionally from the behaviour of the original system and from the behaviour of the processes substituted for actions. We recall that interleaving models of concurrent systems are not suited for defining such an operator in its general form. Instead, we define this operator on several causality based, event oriented models, taking into account the distinction between deadlock and successful termination. Then we investigate the interplay of action refinement with abstraction in terms of equivalence notions for concurrent systems, considering both linear time and branching time approaches. We show that besides the interleaving equivalences, also the equivalences based on steps are not preserved under refinement of actions. We prove that linear time partial order semantics are invariant under refinement. Finally we consider various bisimulation equivalences based on partial orders and show that the finest two of them are preserved under refinement whereas the others are not. Termination sensitive versions of these equivalences are even congruences for action refinement. Received 11 May 1998 / 19 June 2000     

Superposition: composition vs refinement of non-deterministic,action-based systems

The traditional notion of superposition has been used for supporting two distinct aspects of parallel program design: composition and refinement. This is because, when trace-based semantics of concurrency are considered, which is typical of most formal methods, these two relationships are modelled as inclusion between sets of behaviours. However, when forms of non-deterministic behaviour have to be considered, which is the case for component and service-based development, these two aspects do not coincide. In this paper, we show how the two roles of superposition can be separated and supported at the language and semantic levels. For this purpose, we use a categorical formalisation of program design in the language CommUnity that we are also using for addressing architectural concerns, another area in which the distinction between composition and refinement is particularly important.Correspondence and offprint request to: Antónia Lopes, orgdivisionDepartment of Informatics, Faculty of Sciences, University of Lisbon, Campo Grande, 1749-016 Lisbon, Portugal.Received November 2002 Accepted in revised form June 2003 by B.T. Denvir and E. Boiten     

Connection models for the Internet-of-Things

The Internet-of-Things(IoT)is expected to swamp the world.In order to study and understand the emergent behaviour of connected things,effective support for their modelling is needed.At the heart of IoT are flexible and adaptive connection patterns between things,which can naturally be modelled by channel-based coordination primitives,and characteristics of connection failure probabilities,execution and waiting times,as well as resource consumption.The latter is especially important in light of severely limited power and computation budgets inside the things.In this paper,we tackle the IoT modelling challenge,based on a conservative extension of channel-based Reo circuits.We introduce a model called priced probabilistic timed constraint automaton,which combines models of probabilistic and timed aspects,and integrates pricing information.An expressive logic called priced probabilistic timed scheduled data stream logic is presented,so as to enable the specification and verification of properties,which characterize data-flow streams and prices.A small but illustrative IoT case demonstrates the principal benefits of the proposed approach.     

Model-checking user behaviour using interacting components

This article describes a framework to formally model and analyse human behaviour. This is shown by a simple case study of a chocolate vending machine, which represents many aspects of human behaviour. The case study is modelled and analysed using the Maude rewrite system. This work extends a previous work by Basuki which attempts to model interactions between human and machine and analyse the possibility of errors occurring in the interactions. By redesigning the interface, it can be shown that certain kinds of error can be avoided for some users. This article overcomes the limitation of Basuki’s approach by incorporating many aspects of user behaviour into a single user model, and introduces a more natural approach to model human–computer interaction.     

形式化方法B的精化

形式化方法B支持从抽象规约到实现的完整的开发过程，用于开发安全关键的软件系统。给出了B方法精化的定义后，介绍了抽象机的精化过程与方法，结合实例分析了仅使用前向精化的普通精化规则的不完整性，通过引入反向精化提供了完备的精化理论，二者联合起来能够证明任何正确的精化。     

Performance analysis of probabilistic action systems

Formal notations like B or action systems support a notion of refinement. Refinement relates an abstract specification A to a concrete specification C that is as least as deterministic. Knowing A and C one proves that C refines, or implements, specification A. In this study we consider specification A as given and concern ourselves with a way to find a good candidate for implementation C. To this end we classify all implementations of an abstract specification according to their performance. We distinguish performance from correctness. Concrete systems that do not meet the abstract specification correctly are excluded. Only the remaining correct implementations C are considered with respect to their performance. A good implementation of a specification is identified by having some optimal behaviour in common with it. In other words, a good refinement corresponds to a reduction of non-optimal behaviour. This also means that the abstract specification sets a boundary for the performance of any implementation. We introduce the probabilistic action system formalism which combines refinement with performance. In our current study we measure performance in terms of long-run expected average-cost. Performance is expressed by means of probability and expected costs. Probability is needed to express uncertainty present in physical environments. Expected costs express physical or abstract quantities that describe a system. They encode the performance objective. The behaviour of probabilistic action systems is described by traces of expected costs. A corresponding notion of refinement and simulation-based proof rules are introduced. Probabilistic action systems are based on discrete-time Markov decision processes. Numerical methods solving the optimisation problems posed by Markov decision processes are well-known, and used in a software tool that we have developed. The tool computes an optimal behaviour of a specification A thus assisting in the search for a good implementation C.Received September 2002 Accepted in revised form January 2004 by E.C.R. Hehner