Compositional Comparison of Formal Software Specifications Using Transformation Systems

In a model-based software systems development formal specifications of the components of the system are developed. Thereby different specifications are used to represent the different aspects or views of the components, possibly following different paradigms. These heterogeneous viewpoint specifications have to be integrated in order to obtain a consistent global specification of the whole system. In this paper transformation systems are introduced as a common semantic domain where specifications written in different languages can be interpreted and formally compared. A transformation system is a transition system where the transitions are labelled by sets of actions and the states are labelled by algebras representing the data states. Development relations and composition operations for transformation systems are investigated, and it is shown that compatible local developments of components induce a global development of their composition. As an application two specifications of the alternating bit protocol are formally compared component-wise, one given in the process calculus CCS, the other one in the parallel programming language UNITY. Received September 2000 / Accepted in revised form June 2001     

软件开发的形式化方法

随着计算机及软件系统逐步渗透到社会生活的方方面面,对软件可靠性、安全性和保密性的要求也越来越高．本文阐述了形式化方法的定义、重要性及主要研究内容。着重讨论了形式规约方法,以及演绎证明和模型检测等形式验证方法。     

Integrating predicate transition nets with first order temporal logic in the specification and verification of concurrent systems

This paper presents some results of integrating predicate transition nets with first order temporal logic in the specification and verification of concurrent systems. The intention of this research is to use predicate transition nets as a specification method and to use first order temporal logic as a verification method so that their strengths — the easy comprehension of predicate transition nets and the reasoning power of first order temporal logic can be combined. In this paper, a theoretical relationship between the computation models of these two formalisms is presented; an algorithm for systematically translating a predicate transition net into a corresponding temporal logic system is outlined; and a special temporal refutation proof technique is proposed and illustrated in verifying various concurrent properties of the predicate transition net specification of the five dining philosophers problem.     

Case Study: Formal Verification of a Computerized Railway Interlocking

We describe a case study in system-level verification of a computerized railway interlocking developed by ADtranz Spain, installed and put into test use at a subway station in Madrid. The formal modelling and analysis was carried out by personell at ADtranz Sweden using a tool for automatic formal modelling of the interlocking system and the commerical verification software NP-Tools, which is based on St?lmarck's patented proof procedure. The case study took about one man week in total, of which most of the time was spent modelling safety requirements. The analysis discovered an error that had passed the traditional verification phase. The actual analysis time, disproving the safety requirements by supplying a countermodel, was done in a matter of seconds. The corrected software could be proved to fulfil the safety requirements in the same amount of time. This case study is one of many carried out by ADtranz during 1995-98 in the process in which they have replaced the traditional techniques used for system level verification of safety with formal techniques. We give an overview of the formal methods and tools used which today are integrated in the development environment at ADtranz. Received March 1997 / Accepted in revised form July 1998     

What Kind of Verification of Formal Navigation Modelling for Reliable and Usable Web Applications?

In this paper we introduce briefly a notation dedicated to model navigation of Web applications and we discuss some strategies to assess the usability over navigation models built with such as a notation. Our aim with this kind of evaluation is to ensure (prior to implementation) that important users tasks can (or cannot) be performed using the system.     

一种嵌入式实时系统软件的形式化开发方法

领域特征突出的嵌入式实时系统软件开发,既需要严格地保证可靠性又要充分反映实时和交互行为特征,针对这种需要,该文提出了一种从需求分析到体系结构建模直至使用组件技术实现软件的形式化开发方法。文章在介绍了目前的各软件工程领域以及各软件开发阶段中的形式化模型和工具的现状和特点后,引入需求分析的模型和体系结构建模的描述语言,分析其长处和不足,最后对该方法与移动组件结合的前景进行了展望。