The Rigorous Development of a System Version Control Program

A rigorous approach to software development is followed in developing a program to control the various components and versions of systems. This particular approach to systematic program development is known as the Vienna Development Method (VDM). This paper documerits the author's early experiences with VDM on a small, yet nontrivial, application. The functional specification of the version control system is presented in detail. Design decisions taken for a prototype implementation are also included. The version control program developed is based upon the Gandalf System Version Control Environment of Carnegie-Mellon University. Both that system and the subject of this case study support the most common forms of component interdependency relations, and methods of system evolution.     

Informal and formal requirements specification languages: bridgingthe gap

The differences between informal and formal requirements specification languages are noted, and the issue of bridging the gap between them is discussed. Using structured analysis (SA) and the Vienna development method (VDM) as surrogates for informal and formal languages, respectively, two approaches are presented for integrating the two. The first approach uses the SA model of a system to guide the analyst's understanding of the system and the development of the VDM specifications. The second approach proposes a rule-based method for generating VDM specifications from a set of corresponding SA specifications. The two approaches are illustrated through a simplified payroll system case. The issues that emerge from the use of the two approaches are reported     

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.     

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.     

Software prototyping by relational techniques: experiences withprogram construction systems

A method for designing and prototyping program construction systems using relational databases is presented. Relations are the only data structures used inside the systems and for interfaces; programs extensively use relational languages, in particular relational algebra. Two large projects are described. The Ada Relational Translator (ART) is an experimental compiler-interpreter for Ada in which all subsystems, including the parser, semantic analyzer, interpreter, kernel, and debugger, use relations as their only data structure; the relational approach has been pushed to the utmost to achieve fast prototyping in a student environment. Multi-Micro Line (MML) is a tool set for constructing programs for multimicroprocessors' targets, in which relations are used for allocation and configuration control. Both experiences validate the approach for managing teamwork in evolving projects, identify areas where this approach is appropriate, and raise critical issues     

The Specification and Implementation of GKS Application Software in ADA (R)

One of the most important uses of (interactive) computer graphics is as one of the tools available to a User Interface Management System (UIMS) for a variety of user-computer environments (UCE). Typical UCEs in vogue are Programming Support Environments (PSE), Expert System Builders (ESB), Office Automation systems (OAS). This paper concentrates on the conceptual relationship that exists between the users on the one hand and computer systems on the other. Such relationships are to be seen in the context of specific application domains. The two standards, GKS and Ada, are chosen to be the background against which the argument for a Software Methodology based on the Abstract Data Type approach, is presented. This has significant implications for a GKS binding to Ada and the development of GKS application software written in Ada. A collection of colour models is considered in detail.
Ada(R) is a registered trademark of the U.S. Government, Ada Joint Program Office.     

基于数据分解的并发面向对象程序开发方法

提出了一种从VDM-SL(Vienna development method-specification language)规约到并发面向对象程序的开发方法,这种方法基于DD-VDM(data decomposition-Vienna development method).在此基础上提出了虚拟原子、服务并行和内部并行等概念,继而提出一种嵌套面向对象结构来体现这些功能.分别从共享量并行系统和分布并行系统的角度讨论了嵌套面向对象结构的实现技术.     

Critical races in Ada programs

It is noted that critical races in concurrent Ada programs are an insidious source of system errors, and that the Ada language does not have concurrency features to ease the development of critical race-free programs. The authors illustrate this using the CRF language, which extends the Ada language by the addition of a powerful caller selection mechanism. It is this facility that implements a discriminatory mutual exclusion (dimutex) construct, an important feature for building less critical race-prone programs. The MLog language supports the CRF caller selection mechanisms; thus it is convenient as a rapid-prototyping platform. A design method for systematically converting CRF designs into Ada designs is presented. The method uses a mixture of mechanical and creative transformations that are guaranteed not to introduce critical races. D. Helmbold and D. Luckham's (1985) gas-station example is used to illustrate the various approaches to applying the design method     

ARTK-M2: A kernel for Ada tasking requirements: An implementation and an automatic generator

A run-time kernel, ARTK-M2, supporting Ada tasking semantics is discussed; full support for task creation, synchronization, communication, scheduling, and termination is provided, together with all options of the Ada rendezvous. An implementation in Modula-2 is presented and a method for automatically translating Ada programs into semantically equivalent Modula-2 programs with corresponding kernel calls is introduced. A parser generator and an attribute grammar were used for the automatic translation. A subset of the Ada Compiler Validation Capability was processed to test the implementation and to illustrate the translation mechanism. The kernel is applicable to the study of real-time control systems; it can also serve as a baseline for studying implementation alternatives of Ada concepts, such as new scheduling algorithms, and for analysing new language constructs. Work is under way to implement some of the changes to the Ada tasking model being proposed as a result of the language revision (Ada9X). Finally, through proper extensions, ARTK-M2 can form an integral part of programming tools such as an Ada compilation system and a distributed kernel for multi-processing environments.     

Ada program partitioning language: a notion for distributing Adaprograms

Ada Program Partitioning Language (APPL) has been designed as part of Honeywell's Distributed Ada project. The goal of the project is to develop an approach for reducing the complexity of building distributed applications in Ada. In the proposed approach, an application is written as a single Ada program using the full capabilities of the Ada language. It is not necessary to factor the underlying hardware configuration into the program design. Once the program has been completed and tested in the host development environment, it is partitioned into fragments and mapped onto the distributed hardware. The partitioning and mapping are expressed in APPL and do not require changes to the Ada source. The main thrusts of the project include the design of APPL and the development of language translation tools and the run-time system to support Ada and APPL for a distributed target. The authors present an overview of APPL, the goals considered in the design, and issues that impact its implementation     

Administrators and multiprocessor rendezvous mechanisms

This paper discusses rendezvous on multiprocessors. Three different approaches are compared, represented by three specific systems: Ada, Harmony and BNR Pascal. All three permit tasks to run on multiple processors and use blocking communications primitives, but there are significant differences. For example, control over replying to messages out of sequence and over the allocation of tasks to processors is omitted in Ada, but is available in Harmony. The approach represented by BNR Pascal follows a middle road between Harmony and Ada: a low level protocol, invisible to the programmer, is used to ensure communications reliability, but the programmer is aware of when a rendezvous is remote. If performance considerations and verbosity and robustness are ignored, all three approaches are equivalent. To illustrate this equivalence, and to demonstrate clearly the complexity of the Ada rendezvous, an Ada rendezvous administrator written using Harmony is described. A second method of adapting Harmony to Ada is also presented, in which the Harmony primitives are modified to be closer to Ada. In practice, using Harmony primitives directly will usually result in better programs. It is argued that something very much like the rendezvous adminstrator is needed for any actual implementation of the Ada rendezvous.     

An abstract programming language and correctness proofs

The realization of an abstract programming language is a good approach for automating the software production process and facilitating the correctness proof of a software system.

This paper introduces a formal language for programming at the abstract level by combining Pascal with VDM (Vienna Development Method). The notation provided by the language obliges programmers to consider the correctness of programs throughout the whole process of programming, and the proof axiom and rules presented in this paper may be used to prove the correctness of programs. A complete example is given to illustrate how to program using APL and how to prove the correctness of programs using the given axiom and rules.     

Toward value difference metric with attribute weighting

In distance metric learning, recent work has shown that value difference metric (VDM) with a strong attribute independence assumption outperforms other existing distance metrics. However, an open question is whether VDM with a less restrictive assumption can perform even better. Many approaches have been proposed to improve VDM by weakening the assumption. In this paper, we make a comprehensive survey on the existing improved approaches and then propose a new approach to improve VDM by attribute weighting. We name the proposed new distance function as attribute-weighted value difference metric (AWVDM). Moreover, we propose a modified attribute-weighted value difference metric (MAWVDM) by incorporating the learned attribute weights into the conditional probability estimates of AWVDM. AWVDM and MAWVDM significantly outperform VDM and inherit the computational simplicity of VDM simultaneously. Experimental results on a large number of UCI data sets validate the performance of AWVDM and MAWVDM.     

Denotational Semantics of a Simple Model of Eiffel

A simple abstract model of Eiffel is introduced,and its denotational semantics is defined using VDM style.A static analysis approach is presented to treat multiple inheritance and renaming mechanism.Within the framework of denotational semantics introduced in this paper,the key features of Eiffel,such as identification,classification,multiple inheritance,polymorphism and dynamic binding,can be adequately characterized.     

Detection of Ada static deadlocks using Petri net invariants

A method is presented for detecting deadlocks in Ada tasking programs using structural; and dynamic analysis of Petri nets. Algorithmic translation of the Ada programs into Petri nets which preserve control-flow and message-flow properties is described. Properties of these Petri nets are discussed, and algorithms are given to analyze the nets to obtain information about static deadlocks that can occur in the original programs. Petri net invariants are used by the algorithms to reduce the time and space complexities associated with dynamic Petri net analysis (i.e. reachability graph generation)     

HOOD方法与形式化技术的集成研究

ＨＯＯＤ是由欧洲ＥＳＡ公司开发的一种面向对象软件结构设计方法,它使用图形,结构化英语和Ａｄａ伪码来描述系统的设计规约,本文首先概述了ＨＯＯＤ方法的基本概念和对它进行的改进,然后提出了一种集成ＨＯＯＤ和形式化技术的方法,借助该方法可以获得更为严格的软件设计规约,最后简要介绍了其机器支持系统。     

Experimenting with dynamic linking with ADA

An approach to achieving dynamic reconfiguration within the framework of Ada¹ is described. A technique for introducing a kernel facility for dynamic reconfiguration in Ada is illustrated, and its implementation using the Verdix VADS 5.5 Ada compiling system on a Sun3–120 running the 4.3 BSD Unix operating system is discussed. This experimental kernel allows an Ada program to change its own configuration dynamically, linking new pieces of code at run-time. It is shown how this dynamic facility can be integrated consistently at the Ada language level, without introducing severe inconsistencies with respect to the Standard semantics.     

User-friendly syntax: design and presentation

A user-friendly programming system should have a user-friendly syntax; natural and systematic, easy to understand and use. Syntax should allow substitution of semantically similar constructs by each other. Syntax should also be flexible and allow several variants of syntactic notations to reduce the burden of memorizing rigid syntactic notations and to make it possible for a user to think more about ‘what’ instead of ‘how’. Nowadays programming languages, e.g. Ada, do not obey these principles. Their complexity is mainly caused by their nonsystematic and rigid syntax. This together with unformal and ambiguous presentation of syntax makes Ada difficult to use and Ada parsers inefficient. Uniform, natural and flexible syntax, where several variants of syntactic notations and abbreviations are allowed and minor syntactic errors automatically corrected, can be introduced by systematic top-down design using multi-level grammars. Systematic design and presentation allows greatly improved syntax without increasing size of the syntax grammar and the complexity of the parser.