Extending model checkers for hybrid system verification: the case study of SPIN

A hybrid system is a system that evolves following a continuous dynamic, which may instantaneously change when certain internal or external events occur. Because of this combination of discrete and continuous dynamics, the behaviour of a hybrid system is, in general, difficult to model and analyse. Model checking techniques have been proven to be an excellent approach to analyse critical properties of complex systems. This paper presents a new methodology to extend explicit model checkers for hybrid systems analysis. The explicit model checker is integrated, in a non‐intrusive way, with some external structures and existing abstraction libraries, which store and manipulate the abstraction of the continuous behaviour irrespective of the underlying model checker. The methodology is applied to SPIN using Parma Polyhedra Library. In addition, the authors are currently working on the extension of other model checkers. Copyright © 2013 John Wiley & Sons, Ltd.     

Testing with model checkers: a survey

About a decade after the initial proposal to use model checkers for the generation of test cases we take a look at the results in this field of research. Model checkers are formal verification tools, capable of providing counterexamples to violated properties. Normally, these counterexamples are meant to guide an analyst when searching for the root cause of a property violation. They are, however, also very useful as test cases. Many different approaches have been presented, many problems have been solved, yet many issues remain. This survey paper reviews the state of the art in testing with model checkers. Copyright © 2008 John Wiley & Sons, Ltd.     

DDR2内存

在Inlel的计划表中，在2004年普及DDR2内存也是重要的一环，理论上说，DDR2在带宽提升，功耗，超频能力等方面比现有的DDR内存具有明显优势，采用DDR2带来性能提升简直是一定的……遗憾的是，这一幕也许不会很快变成事实，至少目前在i915/925平台上恐怕还难以得到体现。     

Embedded totally self-checking checkers: a practical design

In a totally self-checking (TSC) design, the circuit detects errors by monitoring redundantly coded data/control paths through a TSC checker. A problem arises when not all these code words are on the monitored lines during normal operation. A method of designing checkers that solves this difficulty is proposed. The method uses TSC checkers based on flip-flops instead of using the mostly combinational checkers now available. Two design applications are presented: TSC checkers for arithmetic AN codes, and a TSC iterative logic array     

Issues in using model checkers for test case generation

The use of model checkers for automated software testing has received some attention in the literature: It is convenient because it allows fully automated generation of test suites for many different test objectives. On the other hand, model checkers were not originally meant to be used this way but for formal verification, so using model checkers for testing is sometimes perceived as a “hack”. Indeed, several drawbacks result from the use of model checkers for test case generation. If model checkers were designed or adapted to take into account the needs that result from the application to software testing, this could lead to significant improvements with regard to test suite quality and performance. In this paper we identify the drawbacks of current model checkers when used for testing. We illustrate techniques to overcome these problems, and show how they could be integrated into the model checking process. In essence, the described techniques can be seen as a general road map to turn model checkers into general purpose testing tools.     

一种高性能DDR2控制器的设计与实现

DDR2是由JEDEC制定的新一代DDR内存技术标准。本文深入研究了DDR2的特点和规范,设计并实现了一个支持体并发和Openpage调度策略的高性能DDR2控制器。性能评测结果表明,所设计和实现的DDR2控制器能有效提高访存带宽,降低访存延迟。     

DDR:一种自适应的面向模式的软件体系结构

信息系统必须处于开放、可更改状态以响应对技术和需求的修改。为满足信息系统这种变化和演化的特征,提出了一种自适应的面向模式的软件体系结构,称之为“显示-定义-实现”(DDR)体系结构模式。描述了DDR体系结构模式适合的问题领域,并给出了相应的解决方案和组织结构。DDR体系结构模式由显示层、定义层与实现层组成。显示层是系统数据表现形式的实现,它实现了应用程序显示逻辑。定义层是DDR体系结构模式的核心,它封装了可更改的系统内部成分——通常以元对象的方式表示,所有元对象的集合形成定义层的数据字典。该层还提供了一个对外接口以方便对自身具体内容的修改,即元对象协议。实现层描述了开发应用功能的用户接口,实现了系统的业务逻辑。用DDR体系结构模式实现的系统,是一个自适应性系统,具有主动性、高安全性等特点,有利于系统的维护、扩展与移植。     

Patterns of SO2 emissions: a refinery case study

Air quality modelling is an essential tool for most air pollution studies and the introduction of SO₂ standards creates a need for modelling the dispersion of SO₂. This work deals specifically with the use of the Industrial Source Complex Short Term (ISCST) model at a refinery. The study is performed over a period of 21 days. The first objective of this study was to measure the atmospheric levels of SO₂ and then to compare their values with the international standard limits. The second objective was to evaluate the ISCST model by comparing the calculated and measured concentrations. The third objective was to demonstrate the effect of wind regimes on the dispersion of SO₂ and to determine the spatial distribution of SO₂ over the modelled area. The results showed that the levels of SO₂ were well below the ambient air quality standard. Based on isopleths for SO₂ distribution in the study area (as output from the ISCST model), it can be stated that no health risk is present in areas adjacent to the refinery.     

DDR2存储系统动态匹配技术

随着同步动态随机存储器DDR2 SDRAM性能的日益提高,对存储系统的设计也提出了更高的要求.芯片内部动态电阻匹配技术是高性能DDR2存储系统设计中提高信号传输质量的关键技术.介绍了DDR2存储器中动态匹配技术的电路结构、信号反射分析以及匹配电阻的实现,指出了采用动态匹配技术的存储系统设计中需要着重考虑的关键问题,并通过软件模拟对动态匹配电路和传统的印制板匹配电路的信号进行了分析和对比.     

Structural redocumentation: a case study

Most software documentation typically describes the program at the algorithm and data-structure level. For large legacy systems, understanding the system's architecture is more important. The authors propose a method of reverse engineering through redocumentation that promises to extend the useful life of large systems     

Courseware validation: a case study

Abstract This paper discusses methods used and problems faced in the validation study of LOGICLANDIA , a courseware package for the learning and teaching of predicate logic in Italian upper secondary schools. The courseware underwent a medium scale evaluation process that involved about three hundred students. LOGICLANDIA's validation consisted of three main phases: subjective evaluation, in-house evaluation and field test. The study produced a number of indications of revision of the courseware material, as well as information about effectiveness of the educational approach and satisfaction of students. But rather than going into the details of the results of LOGICLANDIA's evaluation, the paper focuses on problems encountered and adopted solutions that can be generalised to similar cases.     

Brick handling: a case study

A small change in brick dimensions resulted in an increase in the perceived work-load of men loading and unloading pallets of bricks by hand. A laboratory study indicated that the change in brick dimensions required changes in grip pattern in order to unload bricks at the same rate, moving the same number at a time. These changed grip patterns resulted in increased upper body movement, increased chest-muscle activity and higher heart rates. These differences were reflected in higher subjective ratings of fatigue.     

Robustness analysis: a case study

The stability test of polynomials whose coefficients depend multilinearly on interval parameters is considered. The authors describe and compare four brute-force solution approaches. These are eigenvalue calculation, zero exclusion from a specified value set, algebraic tests of real and complex Hurwitz roots, and the parameter space method. They are applied to a simple example with two parameters and third-order polynomial. An interesting feature of the example is that it can have an isolated unstable point. The example may be useful as a benchmark for future approaches to the multilinear problem. All four methods are shown to be feasible for the simple example, but they require effort     

一种DDR SDRAM控制器的设计

在介绍DDR SDRAM控制器设计关键技术的基础上,讨论了一种DDR SDRAM控制器的设计方法.通过一种优化的地址映射策略提高了突发访问效率,采用0.18 μm CMOS工艺流片实现.所设计的DDR SDRAM控制器芯片在PCB板级测试中达到预期设计要求.     

The Rochester checkers player: multimodel parallel programming foranimate vision

It is maintained that to exploit fully the parallelism inherent in animate vision systems, an integrated vision architecture must support multiple models of parallelism. To support this claim, the hardware base of a typical animate vision laboratory and the software requirements of applications are described. A brief overview is then given of the Psyche operating system, which was designed to support multimodel programming. A complex animate vision application, checkers, constructed as a multimodel program under Psyche, is also described. Checkers demonstrates the advantages of decomposing animate vision systems by function and independently selecting an appropriate parallel-programming model for each function     

Software product lines: a case study

A software product line is a family of products that share common features to meet the needs of a market area. Systematic processes have been developed to dramatically reduce the cost of a product line. Such product‐line engineering processes have proven practical and effective in industrial use, but are not widely understood. The Family‐Oriented Abstraction, Specification and Translation (FAST) process has been used successfully at Lucent Technologies in over 25 domains, providing productivity improvements of as much as four to one. In this paper, we show how to use FAST to document precisely the key abstractions in a domain, exploit design patterns in a generic product‐line architecture, generate documentation and Java code, and automate testing to reduce costs. The paper is based on a detailed case study covering all aspects from domain analysis through testing. Copyright © 2000 John Wiley & Sons, Ltd.     

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.     

Incentives in production: a case study

The motivation, rationale, and experiences of implementing an incentive scheme in a large petrochemical plant in the People's Republic of China for the purpose of conserving the consumption of cooling water is described. Experimental implementation in a section of a plant is described in detail. A few incentive-induced features uncovered after analyzing the experimental data are reported. A mathematical model with several variations is presented. A better predictive property of the incentive scheme in comparison to a more conventional method is proved analytically. The effectiveness of the scheme is shown by the amount of water conserved, and by the management's decision for plantwide adoption of the scheme. Practical issues encountered in experimental implementation, extensions of the scheme to more general situations, and theoretical problem inspired by the experiment are discussed     

Measuring software quality: a case study

The National Security Agency's (NSA) mission is to provide support for the security of the United States. Over the years, the Agency has become extremely dependent on the software that makes up its information technology infrastructure. NSA has come to view software as a critical resource upon which much of the world's security, prosperity, and economic competitiveness increasingly rests. To ensure cost effective delivery of high quality software, NSA has analyzed effective quality measures applied to a sample code base of 25 million lines. This case study dramatically illustrates the benefits of code level measurement activities     

Value-based software engineering: a case study

The information technology field's accelerating rate of change makes feedback control essential for organizations to sense, evaluate, and adapt to changing value propositions in their competitive marketplace. Although traditional project feedback control mechanisms can manage the development efficiency of stable projects in well-established value situations, they do little to address the project's actual value, and can lead to wasteful misuse of an organization's scarce resources. The value-based approach to software development integrates value considerations into current and emerging software engineering principles and practices, while developing an overall framework in which these techniques compatibly reinforce each other.