Real-time verification of wireless home networks using bigraphs with sharing

Home wireless networks are difficult to manage and comprehend because of evolving locality, co-locality, connectivity and interaction. We define formal models of home wireless network infrastructure and policies and investigate how they can be used in a network management system designed to provide user-oriented support. We model spatial and temporal behaviour of network interactions and user-initiated network policies and define an online framework for generation of models from network and user-initiated events. The models are expressed in an extension to Milnerʼs bigraphical reactive systems. Analysis of the models is carried out in real-time by a bespoke bigraph reasoning system based on checking predicates, which is encoded as bigraph matching. Real-time model generation and analysis is implemented on the experimental Homework system router and trialled with synthetic and actual network data.     

Pure bigraphs: Structure and dynamics

Bigraphs are graphs whose nodes may be nested, representing locality, independently of the edges connecting them. They may be equipped with reaction rules, forming a bigraphical reactive system (Brs) in which bigraphs can reconfigure themselves. Following an earlier paper describing link graphs, a constituent of bigraphs, this paper is a devoted to pure bigraphs, which in turn underlie various more refined forms. Elsewhere it is shown that behavioural analysis for Petri nets, π-calculus and mobile ambients can all be recovered in the uniform framework of bigraphs. The paper first develops the dynamic theory of an abstract structure, a wide reactive system (Wrs), of which a Brs is an instance. In this context, labelled transitions are defined in such a way that the induced bisimilarity is a congruence. This work is then specialised to Brss, whose graphical structure allows many refinements of the theory. The latter part of the paper emphasizes bigraphical theory that is relevant to the treatment of dynamics via labelled transitions. As a running example, the theory is applied to finite pure CCS, whose resulting transition system and bisimilarity are analysed in detail. The paper also mentions briefly the use of bigraphs to model pervasive computing and biological systems.     

An environment for formal verification based on symbolic computations

We present an environment for formally verifying hardware, based on symbolic computations. This includes a new concurrency model, called the combinational/sequential or C/S concurrency model which has close ties to hardware. We allow fairness constraints and describe methods for specifying them and for formally verifying in their presence. Properties are specified by either CTL formulae or edge-Rabin automata. We give algorithms, in the presence of fairness constraints, for model checking CTL or for checking that the language of our system is contained in the language of a property automation. Finally, techniques are given for hierarchical verification and for detecting errors quickly (early failure detection).     

基于CDM的嵌入式系统描述与模拟验证环境

从嵌入式系统的设计需求出发,提出采用CDM构造嵌入式系统的描述模型,然后根据相关规则将需求文档转换为CDM描述模型、把CDM描述模型转换成SystemC代码,以完成嵌入式系统的模拟验证的方法和实验环境。最后介绍了该方法的一个应用实例。     

An integrated verification and testing environment

A verification and testing environment that includes static analysis, symbolic execution, and dynamic analysis capabilities is presented. Tool integration and co-operation are promoted through use of an intermediate program representation and a system data manager. A substantial user interface aids application of the tools. Their use is guided by a verification and testing methodology on which the system's design is based. The environment has been engineered to support the production of flight control software written in HAL/S. The environment itself is written in Pascal and is designed to be portable. Several development experiences are described. The environment demonstrates that a strong, unified verification and testing environment can be built; it serves as a basis for future investigations.     

A virtual reality-based experimentation environment for the verification of human-related factors in assembly processes

This paper investigates the use of virtual reality (VR)-based methods for the verification of performance factors related to manual assembly processes. An immersive and interactive virtual environment has been created to provide functionality for realistic process experimentation. Ergonomic models and functions have been embedded into the VR environment to support verification and constrain experimentation to ergonomically acceptable conditions. A specific assembly test case is presented, for which a semi-empirical time model is developed employing statistical design experimentation in the virtual environment. The virtual experimentation results enable the quantification and prediction of the influence of a number of process parameters and their combination at the process cycle time.     

Efficient debugging in a formal verification environment

In this paper, we emphasize the importance of efficient debugging in formal verification and present capabilities that we have developed in order to aid debugging in Intel’s Formal Verification Environment. We have given the name “Counter-Example Wizard” to the bundle of capabilities that we have developed to address the needs of the verification engineer in the context of counter-example diagnosis and rectification. The novel features of the Counter-Example Wizard are the multi-value counter-example annotation, constraint-based debugging, and multiple counter-example generation mechanisms. Our experience with the verification of real-life Intel designs shows that these capabilities complement one another and can help the verification engineer diagnose and fix a reported failure. We use real-life verification cases to illustrate how our system solution can significantly reduce the time spent in the loop of model checking, specification, and design modification. Published online: 21 February 2003     

An inductive characterization of matching in binding bigraphs

We analyze the matching problem for bigraphs. In particular, we present a sound and complete inductive characterization of matching in bigraphs with binding. Our results yield a specification for a provably correct matching algorithm, as needed by our prototype tool implementing bigraphical reactive systems.     

基于交易级建模的ATA控制器功能验证方法研究

交易级建模技术适用于构建大规模电路系统的功能验证平台.结合C 天生的类继承机制和SystemC的接口通道机制,基于该建模技术的ATA控制器验证平台成功实现了随机化的交易级验证,降低了设计模块间通信的复杂度,结构上具有良好的可扩展性和可重用性.着重阐述该验证平台中抽象通道与适配器的通用设计方法,提出了一种基于面向对象技术的创新的验证平台设计模式,并分析了交易级建模和RTL建模之间的区别以及交易级建模技术在提高验证效率上的优势.     

A verification tool for ERLANG

This paper presents an overview of the main results of the project Verification of ERLANG Programs , which is funded by the Swedish Business Development Agency (NUTEK) and by Ericsson within the ASTEC (Advanced Software TEChnology) initiative. Its main outcome is the ERLANG Verification Tool (EVT), a theorem prover which assists in obtaining proofs that ERLANG applications satisfy their correctness requirements formulated as behavioural properties in a modal logic with recursion. We give a summary of the verification framework as supported by EVT, discuss reasoning principles essential for successful proofs such as inductive and compositional reasoning, and an efficient treatment of side-effect-free code. The experiences of applying the tool in an industrial case study are summarised, and an approach for supporting verification in the presence of program libraries is outlined.EVT is essentially a classical proof assistant, or theorem-proving tool, requiring users to intervene in the proof process at crucial steps such as stating program invariants. However, the tool offers considerable support for automatic proof discovery through higher-level tactics tailored to the particular task of the verification of ERLANG programs. In addition, a graphical interface permits easy navigation through proof tableaux, proof reuse, and meaningful feedback about the current proof state, to assist users in taking informed proof decisions.     

A challenge for atomicity verification

An unpublished algorithm of Haldar and Vidyasankar implements an atomic variable of an arbitrary type T for one writer and one reader by means of 4 unsafe variables of type T, three two-valued safe variables, and one three-valued regular variable. We present this algorithm, and prove its correctness by means of a refinement towards a known specification of an atomic variable. The refinement is a composition of refinement functions and a forward simulation. The correctness proof requires many nontrivial invariants. In its construction, we relied on the proof assistant PVS for the administration of invariants and proofs and the preservation of consistency.     

A methodology for efficient hardware verification

We present a methodology which helps structure the design and verification of hardware circuits. Our methodology supports reusable proofs of hardware components, provides for multiple implementations of the same specification, and allows both bottom up and top down verification styles. We provide mechanical assistance for our methodology in the Nuprl proof development system. Our method exploits Nuprl's rich type theory to encode the specification of a module in the type of the module. This allows us to elegantly describe parameterized hardware modules. The methodology is efficient because: the automated support reduces the amount of information that users must provide and the use of parameterized hardware modules eliminates redundant reasoning among proofs of hardware components. In this paper we explain our methodology and illustrate our approach with several examples of circuit verification.     

Speaker verification in sensor and acoustic environment mismatch conditions

Our initial speaker verification study exploring the impact of mismatch in training and test conditions finds that the mismatch in sensor and acoustic environment results in significant performance degradation compared to other mismatches like language and style (Haris et al. in Int. J. Speech Technol., 2012). In this work we present a method to suppress the mismatch between the training and test speech, specifically due to sensor and acoustic environment. The method is based on identifying and emphasizing more speaker specific and less mismatch affected vowel-like regions (VLRs) compared to the other speech regions. VLRs are separated from the speech regions (regions detected using voice activity detection (VAD)) using VLR onset point (VLROP) and are processed independently during training and testing of the speaker verification system. Finally, the scores are combined with more weight to that generated by VLRs as those are relatively more speaker specific and less mismatch affected. Speaker verification studies are conducted using the mel-frequency cepstral coefficients (MFCCs) as feature vectors. The speaker modeling is done using the Gaussian mixture model-universal background model and the state-of-the-art i-vector based approach. The experimental results show that for both the systems, proposed approach provides consistent performance improvement on the conversational approach with and without different channel compensation techniques. For instance, with IITG-MV Phase-II dataset for headphone trained and voice recorder test speech, the proposed approach provides a relative improvement of 25.08?% (in EER) for the i-vector based speaker verification systems with LDA and WCCN compared to conventional approach.