Testing from a Z Specification

This paper looks at the formal analysis of Z specifications in order to enhance the testing process. An algorithm is given that rewrites the specification to a form from which both a partition of the input domain and the states of a finite state automaton model can be derived. Test cases can be derived from the former and an automated system to control the testing process can be based upon the latter. © 1997 by John Wiley & Sons, Ltd.     

服务组合的代数规约

现有的服务组合描述途径不能有效地验证和测试组合正确性,针对这一问题,提出了一个代数规约方法,引入规约包机制扩展面向服务代数规约语言SOFIA以支持该方法。用代数规约单元描述服务系统中的各种实体,其中基调部分定义实体的语法和结构,公理部分定义其功能和行为特性。与一个服务相关的规约单元封装在一个包中或拆分在几个相互引用的包中,每个包形成一个命名空间。当多个服务组合在一起时,以这些服务的代数规约包为基础,一方面抽象地定义组合服务的交互过程和语义,形成描述服务组合实现方式的实现规约包;另一方面抽象地定义组合服务对外接口及其功能语义,形成描述组合服务需求的抽象规约包。在实现规约和抽象规约的双元结构基础上,进一步定义了实现规约和抽象规约之间必须满足的“实现”关系,证明了满足实现关系可以保证实现的正确性,从而为服务组合的可验证性和可测试性奠定了理论基础。最后结合实例分析阐述了用代数规约描述服务组合的抽象性、可表达性和可验证性。     

A rigorous method for test templates generation from object-oriented specifications

This paper describes a rigorous method that investigates the suitability of formal specifications written in Object-Z specification language for testing object-oriented software implementation in a black-box fashion. The insight gained in the formalization of a model, the inherent abstractions, and formally specified intended behaviours and exceptions lead to the generation of test templates that are free from any implementation bias. The method described in this paper is an extension of the one proposed by Stocks and Carrington. In particular, the focus of the paper is on generating test templates for composite operations in an Object-Z specification. The method is illustrated using the specification for an electronic mail system. The specification and the test templates generated for the electronic mail system show several interesting properties of the application that require considerable attention during testing. Copyright © 2001 John Wiley & Sons, Ltd.     

Generation of execution sequences for modular time critical systems

We define methods for generating execution sequences for time-critical systems based on their modularized formal specification. An execution sequence represents a behavior of a time critical system and can be used, before the final system is built, to validate the system specification against the user requirements (specification validation) and, after the final system is built, to verify whether the implementation satisfies the specification (functional testing). Our techniques generate execution sequences in the large, in that we focus on the connections among the abstract interfaces of the modules composing a modular specification. Execution sequences in the large are obtained by composing execution sequences in the small for the individual modules. We abstract from the specification languages used for the individual modules of the system, so our techniques can also be used when the modules composing the system are specified with different formalisms. We consider the cases in which connections give rise to either circular or noncircular dependencies among specification modules. We show that execution sequence generation can be carried out successfully under rather broad conditions and we define procedures for efficient construction of execution sequences. These procedures can be taken as the basis for the implementation of (semi)automated tools that provide substantial support to the activity of specification validation and functional testing for industrially-sized time critical systems     

Formal specification and testing: A case study

Z is a formal notation for writing system specifications that has been growing in popularity over recent years. This paper examines some of the issues involved in applying a ‘partition based’ testing method to a system specified in Z. Details of an extensive case study are given, from specification and implementation of the system to the development and execution of test cases. The strategy is found to have benefits compared to those based on less formal specifications, but there are limitations to the approach, and difficulties that need addressing.     

Composition and synthesis with a formal interactor model

This paper discusses the formal specification of interactors, which are primitive abstractions of user interface software, and focuses on the formal aspects of their composition. The composition of interactors is discussed formally in the framework of the Abstraction-Display-Controller (ADC) interactor model. The ADC model has been defined as a LOTOS specification template tailored for specifying user interface software. LOTOS behaviour expressions combining instances of this template specify the composition of interactors to model complex user interfaces. Synthesis is defined as a transformation of these behaviour expressions which supports the generic structure of the ADC model while preserving the meaning of the specified behaviour. Further, the notion of abstract views of interactors is introduced. It is shown how abstract views are themselves primitives for specifying complex interface architectures.     

Object-oriented specification of user interfaces

This paper presents an object-oriented approach for the specification of graphical user interfaces. Specification starts with the analysis of the end user's operations. The user interface is then designed on the basis of this analysis. Operation analysis is followed by structure and component specification which presents the dialogue structure of the application and the contents of each dialogue. Visualization produces the final screen layouts, and task specification documents the usage of the user interface for the purpose of creating user's guides. The method presented in this paper makes it easier for a designer to take the end user's needs into account. Still, it does not automatically guarantee good quality user interfaces. The top-down nature of the method allows the designer to concentrate on the most important aspects of the user interface and split the design procedure into manageable pieces. Also, the visibility of the process allows the designer to communicate with other people while specifying the user interface. This paper connects the method with the object-oriented specification of entire applications. It briefly explains the connections with object-oriented analysis and design, and demonstrates how to implement the specified user interface in an object oriented fashion. The approach presented in this paper is being applied in the development of a large network management system with about two million lines of C++ code running in the XII environment. Still, the method does not require the specification being implemented with any specific windowing system. The only requirement is that the user interface is based on graphical elements, such as dialogues, push-buttons and text fields.     

Structuring formal specifications—a lesson relearned

Specifications written in the formal specification language Z often make use of a form of decomposition that is novel to programmers. A published Z specification is rewritten using the form of decomposition familiar to programmers. Whenever decomposition is used, there must be some strategy for deciding what is to go in one component and what is to go in another. At the highest level, the strategy underlying the rewritten specification is the well-known strategy of separating user interface issues from deeper system functionality issues. The effectiveness of the strategy is put to a simple test by showing how a modification to the interface can be supported by a modification to only part of the specification. The conclusions drawn are that care over decomposition is important in specifications, just as it is in programs, and that lessons learned from programming about effective decomposition strategies can be applicable at the specification level, too. In particular, the lesson relearned is that it is important to separate information about a system's functionality from information about how this functionality is presented to users.     

基于消息机制的自动化黑盒测试方法研究*

如何对人机交互频繁的软件如三维CAD软件进行自动化黑盒测试是一个富有挑战性的研究课题。基于Windows消息机制提出一种针对图形用户界面软件进行自动化黑盒测试的构造模型,该模型通过拦截Windows底层的各种消息,同时依据相应的流程规约和生成算法将消息序列进行重组,从而派生出大量的测试用例,然后以重构后的衍生消息序列驱动被测试系统自动运行,达到自动测试的目的。实验结果表明,基于该思路构建的测试系统具有良好的测试效果。     

基于消息机制的自动化黑盒测试方法研究

如何对人机交互频繁的软件如三维CAD软件进行自动化黑盒测试是一个富有挑战性的研究课题。基于Windows消息机制提出一种针对图形用户界面软件进行自动化黑盒测试的构造模型,该模型通过拦截Windows底层的各种消息,同时依据相应的流程规约和生成算法将消息序列进行重组,从而派生出大量的测试用例,然后以重构后的衍生消息序列驱动被测试系统自动运行,达到自动测试的目的。实验结果表明,基于该思路构建的测试系统具有良好的测试效果。     

Specification and testing using generalized machines: a presentation and a case study

Although testing is a major part of software development, it rarely gets the attention it deserves from researchers, partly because its foundations are weak and ill-understood. The principal purpose of testing is to detect (and then remove) faults in a software system. However, very few of the existing methods allow the tester to make any precise statement about the type or number of faults that remain undetected after testing is completed. In particular, none of the main techniques used by the software industry can give serious guarantees that a system is fault-free after testing has been completed. This paper advocates the use of a formal method both as a specification language and as the basis of a test data selection strategy. It presents a new method for generating test cases from this type of formal specification that provides a more convincing answer to the problem of detecting all faults in a software system. The method is reductionist in the sense that it guarantees that a system is fault-free provided that its components are fault-free; in turn, the same method could be used to test the resulting sub-systems, so the reduction will continue until the components considered are either known to be correct or are fairly simple pieces of code that can be successfully tested using traditional methods. The formal method used, X-machines, is a blend of finite state machines, data structures and processing functions and provides a simple and intuitive way of specifying computer systems. The use of X-machines as a specification tool and the testing method are illustrated with a case study. © 1998 John Wiley & Sons, Ltd.     

基于有限自动机的面向对象软件规约测试

面向对象方法已经逐步代替基于过程的方法成为软件开发的主流,然而面向对象软件的测试和维护代价却并没有因此而减少.虽然在面向对象软件测试方面做了很多的研究工作,但是大多数针对面向对象软件测试的研究都是针对单一类的测试,而不是更高层次上的对面向对象软件规约的测试.提出了一种基于有限自动机的测试框架以测试面向对象软件规约中存在的不完整性和不一致性.该方法有别于公式证明和模型检查,它直接依据可执行的有限自动机来执行测试而不是人工的推导公式证明也不产生大量的状态空间.     

Statechart testing method for aircraft control systems

A number of current control systems for aircraft have been specified with statecharts. The risk of failures requires the use of a formal testing approach to ensure that all possible faults are considered. However, testing the compliance of an implementation of a system to its specification is dependent on the specification method and little work has been reported relating to the use of statechart-specific methods. This paper describes a modification of a formal testing method for extended finite-state machines to handle the above problem. The method allows one to demonstrate correct behaviour of an implementation of some system, with respect to its specification, provided certain specific requirements for both of them are satisfied. The case study illustrates these and shows the applicability of the method. By considering the process used to develop the system it is possible to reduce the size of the test set dramatically; the method to be described is easy to automate. Copyright © 2001 John Wiley & Sons, Ltd.     

A safe regression testing approach for safety critical systems

Regression testing is important activity during the software maintenance to deal with adverse effects of changes. Our approach is important for safety critical system as usually formal methods are preferred and highly recommended for the safety critical systems but they are also applied for the systems development of other than critical system. Our approach is based on Regression testing using VDM++ which takes two VDM++ specifications, one baseline and other delta (Changed) along with test suite for the baseline version. It compares both versions by using comparator module, identifies the change. By analyzing the change we classify the test cases from original test suite into obsolete, re-testable, and reusable test cases. Our scope is at unit level i.e. at class level. Our approach gets two versions of VDM++ specification and returns regression test suite for the delta version. Our approach distinguishes test cases which are still effective for the delta version of VDM++ specification and it differs from re-test all strategy as it can distinguish the test cases and identifies test cases which are useful for delta version. Test cases reusability and test case reduction is the main objective of our approach. Our approach presents how to perform regression testing using VDM++ specification during the maintenance of systems.     

From Object‐Z specifications to ClassBench test suites

This paper describes a method for specification‐based class testing that incorporates test case generation, execution, and evaluation based on formal specifications. This work builds on previous achievements in the areas of specification‐based testing and class testing by integrating the two within a single framework. The initial step of the method is to generate test templates for individual operations from a specification written in the Object‐Z specification language. These test templates are combined to produce a finite state machine for the class that is used as the basis for test case execution using the ClassBench test execution framework. An oracle derived from the Object‐Z specification is used to evaluate the outputs. The method is explained using a simple example and its application to a more substantial case study is also discussed. Copyright © 2000 John Wiley & Sons, Ltd.     

面向对象软件簇级的一种动态测试工具的设计与实现

提出一种基于规格说明的面向对象簇级动态测试的新方法，并将它完全嵌入到被测试程序的解释器中，从而构成了一个解释型簇级测试工具，本文描述运用面向对象的方法设计和实现该测试工具的一个原型系统。     

Integral: Petri-net approach to distributed software development

As the architecture of modern software systems continues to evolve in a distributed fashion, the development of such systems becomes increasingly complex, which requires the integration of more sophisticated specification techniques, tools, and procedures into the conventional methodology. An essential capability of an integrated software development environment is a formal specification method to capture effectively the system's functional requirements as well as its performance requirements. A validation and verification (V&V) system based on a formal specification method is of paramount importance to the development and maintenance of distributed systems.

There has been recent interest in integrating software techniques and tools at the specification level. It is also noted that an effective way of achieving such integration is by using wide-spectrum specification techniques. In view of these points, an integrated V&V system, called Integral, is presented that provides comprehensive and homogeneous analysis capabilities to both specification and testing phases of the life-cycle of distributed software systems. The underlying software model that supports various V&V activities in Integral is primarily based on Petri nets and is intended to be wide spectrum. The ultimate goal of this research is to demonstrate to the software industry, domestic or foreign, the availability and applicability of a new Petri-net-based software development paradigm. Integral is a prototype V&V system to support such a paradigm.