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.     

Angelic Nondeterminism and Unifying Theories of Programming

Hoare and He's unifying theories of programming (UTP) is a model of alphabetised relations expressed as predicates, which supports development in several programming paradigms. The aim is the unification of languages and techniques, so that we can benefit from results in different contexts. In this paper, we investigate the integration of angelic nondeterminism in the UTP; we propose the unification of a model of binary multirelations, which is isomorphic to the monotonic predicate transformers model and can express angelic and demonic nondeterminism.     

形式化方法Designware、B的比较

用形式化方法开发软件是提高软件可靠性和开发效率的革命性途径。Designware、B是两种支持软件开发全过程的形式化方法。对它们的规约描述方法、规约求精方式、开发步骤进行比较,最后分析这两种方法各自的优缺点。     

Specification, Validation, and Synthesis of Email Agent Controllers: A Case Study in Function Rich Reactive System Design

With a few exceptions, previous formal methods for reactive system analysis have focused on finite state machines represented in terms of boolean states and boolean next-state functions. By contrast, in many reactive system domains requirements engineers and developers think in terms of complex data types and expressive next-state functions. Formal methods for reactive system design must be extended to meet their needs as well. I term a reactive system function rich if expressing its state, next-state function, or output function naturally requires this higher expressive power. ISAT, a prototype formal-methods based tool environment, is intended to assist in the creation and validation of function rich reactive systems. This paper describes a case study I have carried out using ISAT to design, validate, synthesize, and evolve controllers for the email agent components making up a novel spam-free email system that I deployed in a user trial in July 1999. The trial has been running since, with high availability, through several evolutionary specification changes and resulting software releases. The case study illustrates the use of a mix of validation techniques, from scenario simulation and coverage through static analysis and theorem proving, and discusses the value each technique adds. In addition to summarizing ISAT and the trial, this paper discusses tool requirements placed by the domain and task, the simple and powerful platform/controller/pure-functions software architecture of the components, and lessons learned.     

A Constructive Graphical Model Approach for Knowledge-Based Systems: A Vehicle Monitoring Case Study

Graphical models have been widely applied to uncertain reasoning in knowledge-based systems. For many of the problems tackled, a single graphical model is constructed before individual cases are presented and the model is used to reason about each new case. In this work, we consider a class of problems whose solution requires inference over a very large number of models that are impractical to construct a priori. We conduct a case study in the domain of vehicle monitoring and then generalize the approach taken. We show that the previously held negative belief on the applicability of graphical models to such problems is unjustified. We propose a set of techniques based on domain decomposition, model separation, model approximation, model compilation, and re-analysis to meet the computational challenges imposed by the combinatorial explosion. Experimental results on vehicle monitoring demonstrated good performance at near-real-time.     

一个机载软件需求形式化建模与分析实例研究

现代民机机载软件系统的功能与复杂度在快速增长的同时还必须满足更严格的安全标准, 使得在机载软件需求层级必须进行诸如一致性、完整性等分析与验证成为重要的挑战. 工作基于一个自主设计实现的面向机载软件自然语言需求形式化建模与分析工具平台(ART)展开对座舱显控软件子系统(EICAS)需求的建模与分析, 包括: ART工具平...     

Fun with FireWire: A Comparative Study of Formal Verification Methods Applied to the IEEE 1394 Root Contention Protocol

Formal Aspects of Computing - The IEEE 1394 Root Contention Protocol is an industrial leader election algorithm for two processes in which probability, real time and parameters play an important...     

A formal software development approach using refinement calculus

The advantage of COOZ(Complete Object-Oriented Z) is to specify large scale software,but it does not support refinement calculus.Thus its application is comfined for software development.Including refinement calculus into COOZ overcomes its disadvantage during design and implementation.The separation between the design and implementation for structure and notation is removed as well .Then the software can be developed smoothly in the same frame.The combination of COOZ and refinement calculus can build object-oriented frame,in which the specification in COOZ is refined stepwise to code by calculus.In this paper,the development model is established.which is based on COOZ and refinement calculus.Data refinement is harder to deal with in a refinement tool than ordinary algorithmic refinement,since data refinement usually has to be done on a large program component at once.As to the implementation technology of refinement calculus,the data refinement calculator is constructed and an approach for data refinement which is based on data refinement calculus and program window inference is offered.     

Contract-based Mutation Testing in the Refinement Calculus

This article discusses mutation testing strategies in the context of refinement. Here, a novel generalization of mutation testing techniques is presented to be applied to contracts ranging from formal specifications to programs. It is demonstrated that refinement and its dual abstraction are the key notions leading to a precise and yet simple theory of mutation testing. The refinement calculus of Back and von Wright is used to express the concepts like contracts, useful mutations, test-cases and test-coverage.     

Monitoring of Probabilistic Timed Property Sequence Charts

Run‐time monitoring is an important technique to detect erroneous run‐time behaviors. Several techniques have been proposed to automatically generate monitors from specification languages to check temporal and real‐time properties. However, monitoring of probabilistic properties still requires manual generation. To overcome this problem, we define a formal property specification language called Probabilistic Timed Property Sequence Chart (PTPSC). PTPSC is a probabilistic and timed extension of the existing scenario‐based specification formalism Property Sequence Chart (PSC). We have defined a formal grammar‐based syntax and have implemented a syntax‐directed translator that can automatically generate a probabilistic monitor which combines timed B”uchi automata and a sequential statistical hypothesis test process. We validate the generated monitors with a set of experiments performed with our tool WS‐PSC Monitor. Copyright © 2011 John Wiley & Sons, Ltd.     

How to Implement a Safe Real-Time System:The OBSERV Implementation of the Production Cell Case Study

The Production Cell example was chosen by FZI (the Computer Science Research Center), in Karlsruhe. to examine the benefits of formal methods for industrial applications. This example was implemented in more than 30 formalisms. This paper describes the implementation of the Production Cell in OBSERV. The OBSERV methodology for software development is based on rapid construction of an executable specification, or prototype, of a system, which may be examined and modified repeatedly to achieve the desired functionality. The objectives of OBSERV also include facilitating a smooth transition to a target system, and providing means for reusing specification, design, and code of systems, particularly real-time reactive systems. In this paper we show how the methods used in the OBSERV implementation address the requirements imposed by reactive systems. We describe the OBSERV implementation of the Production cell, explain design decisions, with special emphasis on reusability and safety issues. We demonstrate how to take care of safety and liveness properties required for this example. These properties are checked by means of simulation and formally proved with a model checker.     

EasyModel: A Refinement-Based Modeling and Verification Approach for Self-Adaptive Software

Journal of Computer Science and Technology - Self-adaptive software (SAS) is gaining popularity as it can reconfigure itself in response to the dynamic changes in the operational context or itself....     

Decision Procedures for the Security of Protocols with Probabilistic Encryption against Offline Dictionary Attacks

We consider the problem of formal automatic verification of cryptographic protocols when some data, like poorly chosen passwords, can be guessed by dictionary attacks. First, we define a theory of these attacks and propose an inference system modeling the deduction capabilities of an intruder. This system extends a set of well-studied deduction rules for symmetric and public key encryption, often called Dolev–Yao rules, with the introduction of a probabilistic encryption operator and guessing abilities for the intruder. Then, we show that the intruder deduction problem in this extended model is decidable in PTIME. The proof is based on a locality lemma for our inference system. This first result yields to an NP decision procedure for the protocol insecurity problem in the presence of a passive intruder. In the active case, the same problem is proved to be NP-complete: we give a procedure for simultaneously solving symbolic constraints with variables that represent intruder deductions. We illustrate the procedure with examples of published protocols and compare our model to other recent formal definitions of dictionary attacks.     

一种基于抽象与精化技术的Web服务组合验证方法

模型检测因其自动化程度高、能够提供反例路径等优势,被广泛应用于Web服务组合的兼容性验证。本文针对模型检测过程中存在的状态爆炸问题,在传统的模型检测方法中引入谓词抽象和精化技术,提出了一种针对Web服务组合的抽象精化验证框架。使用谓词抽象技术对原子Web服务抽象建模,将各Web服务抽象模型组合成组合抽象模型;将模型检测后得到的反例在各原子Web服务上做投影操作,对投影反例进行确认;对产生伪反例的Web服务抽象模型进行精化,生成新的组合抽象模型,再次对性质进行验证。最后通过实例分析说明基于抽象精化技术的Web服务组合验证框架在缓解状态爆炸问题上的可行性。     

方块苗文动态构造方法的形式化描述

针对如何在计算机中生成和显示方块苗文的问题,提出了一种方块苗文动态构造方法,给出了该方法的基本原理,定义了实现方块苗文动态构造所需要的操作符,并以谓词规则的形式对方块苗文动态构造变换操作进行了描述。该方法仅需存储方块苗文构件及独体字的显现字符,通过对显现字符进行上下组合、左右组合、侧围组合来实现方块苗文的动态构造,为方块苗文字库中字形构件提取及合体字自动生成技术提供了重要支持。     

Formal hardware verification methods: A survey

Growing advances in VLSI technology have led to an increased level of complexity in current hardware systems. Late detection of design errors typically results in higher costs due to the associated time delay as well as loss of production. Thus it is important that hardware designs be free of errors. Formal verification has become an increasingly important technique towards establishing the correctness of hardware designs. In this article we survey the research that has been done in this area, with an emphasis on more recent trends. We present a classification framework for the various methods, based on the forms of the specification, the implementation, and the proff method. This framework enables us to better highlight the relationships and interactions between seemingly different approaches.