软件形式化开发方法的选择策略研究

随着软件形式化方法的不断发展,各种各具特色的形式化方法涌现出来,为了解决在具体的系统开发中如何选取合适的形式化方法,对目前较为流行的几种形式化方法RSL,B,VDM,Z的特点进行对比分析,然后针对不同的软件开发人员和所需开发系统的不同,给出了适合用形式化方法开发的情况和如何选择合适的形式化开发方法。     

An alternate method for using a visual discrimination model (VDM) to optimize soft-copy display image quality

Researchers have developed visual discrimination models (VDMs) that can predict a human observer's ability to detect a target object superposed on an image. These models incorporate sophisticated knowledge of the properties of the human visual system. In the predictive approach, termed conventional VDM usage, two input images with and without a target are analyzed by an algorithm that calculates a just-noticeable-difference (JND) index, which is a taken as a measure of the detectability of the target. A new method of using the VDM is described, termed channelized VDM, which involves finding the linear combination of the VDM-generated channels (which are not used in conventional VDM analysis) that has optimal classification ability between normal and abnormal images. The classification ability can be measured using receiver operating characteristic (ROC) or two alternative forced choice (2AFC) experiments, and in special cases they can also be predicted by signal detection theory (SDT) based model-observer methods. In this study simulated background and nodule containing regions were used to validate the new method. It was found that the channelized VDM predictions were in excellent qualitative agreement with human-observer validated SDT predictions. Either VDM method (conventional or channelized) has potential applicability to soft-copy display optimization. An advantage of any VDM-based approach is that complex effects, such as visual masking, are automatically accounted for, which effects are usually not included in SDT-based methods.     

基于敏捷建模的形式化需求分析方法

软件需求分析是软件生命周期中最关键的一步。传统的需求建模方法主要有两个重大的缺陷：1）非形式化的需求描述常常导致需求的歧义性和不一致性,因而难以确认和验证;2）易变一牲,需求变更及其连锁反应是对项目质量、进度乃至合同履行影响最大的风险因素。本文针对软件需求分析阶段的难点,通过将形式化方法和敏捷建模理论相结合,提出一套基于敏捷建模的形式化需求分析方法。     

The Application of VDM to the Industrial Development of Firmware for a Smart Card IC Chip

We have applied the formal speci.cation language in the development of the .rmware of the smart card IC chip for embedding in mobile phone. We report on an in-dustrial application of formal methods to the development of a complex system, namely the .rmware for the “Mobile FeliCa” smart card IC chip. The use of formal techniques, specif-ically the Vienna Development Method (VDM), was aimed at raising the quality of system speci.cations by reducing ambiguity and improving communications between engineers. De-velopment data gathered during the life cycle con.rm the e.ectiveness of a lightweight formal method in contributing to the quality of the deliverables in early development stages. No software speci.cation problems have, to date, been reported since .rst release (over 100 million mobile phones have the chip embedded).     

The formal semantics of ISO VDM-SL

This paper provides an overview of the formal semantics of VDM-SL which currently is being standardized by ISO. This is a specification language used in the formal method known as the Vienna Development Method (or simply VDM). In this paper we will focus on the foundations and the semantics of a rather unique combination of looseness and recursion.     

VDM和Z两种规范描述语言的比较

本文以以关系数据库的规范为例，详细讨论了两种重要的规范描述语言ＶＤＭ和Ｚ的主要区别，对它们的共性和发展史也作了简单介绍。     

基于形式化方法的快速原型技术

本文从传统的软件生存周期模型的弊病出发，分析与综述了快速原型软件开发方法的原理、技术及其应用，并与其它模型作了比较，提出了明确的观点．然后，提出了正在开发中的一个基于形式化方法的快速原型软件工程环境（ＳＤＳ），介绍了它的组成，基本特点及应用实例．     

Hoare's logic and VDM

A relational framework which unifies Hoare's logic and VDM is presented. Within this framework a partial correctness version of VDM is defined. It is argued that this partial correctness version of VDM is intuitive and consistent with the original total correctness version. Furthermore it is shown how both partial and total correctness formulae and specifications can be translated from Hoare's logic into VDM and vice versa. VDM's satisfiability requirement is briefly discussed, and a similar condition for Hoare's logic is defined.:Supported by NWO/SION project 612-316-103: Fault Tolerance: Paradigms, Models, Logics, Construction.