Search

This paper is concerned with the need for computer-based tools which help human designers formulate formal process-oriented specifications. It first determines some attributes of a suitable process-oriented specification language, then examines the reasons why specifications would still be difficult to write in such a language in the absence of formulation tools. The key to overcoming these difficulties seems to be the careful introduction of informality based on partial, rather than complete, descriptions and the use of a computer-based tool that uses context extensively to complete these descriptions during the process of constructing a well-formed specification. Some results obtained by a running prototype of such a computer-based tool on a few informal example specifications are presented and, finally, some of the techniques used by this prototype system are discussed. [ABSTRACT FROM AUTHOR]

This paper illustrates how software can be described precisely using LD-relations, how these descriptions can be presented in a readable manner using tabular notations, and one way such descriptions can be used to test programs. We describe an algorithm that can be used to generate a test oracle from program documentation, and present the results of using a tool based on it to help test part of a commercial network management application. The results demonstrate that these methods can be effective at detecting errors and greatly increase the speed and accuracy of test evaluation when compared with manual evaluation. Such oracles can be used for unit testing, in situ testing, constructing self-checking software, and ensuring consistency between code and documentation. [ABSTRACT FROM AUTHOR]

We report on a formal requirements analysis experiment involving an avionics control system. We describe a method for specifying and verifying real-time systems with PVS. The experiment involves the formalization of the functional and safety requirements of the avionics system as well as its multilevel verification. First level verification demonstrates the consistency of the specifications whilst the second level shows that certain system safety properties are satisfied by the specification. We critically analyze methodological issues of large scale verification and propose some practical ways of structuring verification activities for optimizing the benefits. [ABSTRACT FROM AUTHOR]

The typical correspondence between a concrete representation and an abstract conceptual value of an abstract data type (ADT) variable (object) is a many-to-one function. For example, many different pointer aggregates give rise to exactly the same binary tree. The theoretical possibility that this correspondence generally should be relational has long been recognized. By using a nontrivial ADT for handling an optimization problem, we show why the need for generalizing from functions to relations arises naturally in practice. Making this generalization is among the steps essential for enhancing the practical applicability of formal reasoning methods to industrial-strength software systems. [ABSTRACT FROM AUTHOR]

This paper describes the development of a formal security policy model in Z for the NATO Air Command and Control System (ACCS): a large, distributed, multilevel-secure system. The model was subject to manual validation, and some of the issues and lessons in both writing and validating the model are discussed. [ABSTRACT FROM AUTHOR]

This paper presents a formal specification in the Z notation for a safety-critical control system. It describes a particular medical device but is quite generic and should be widely applicable. The specification emphasizes safety interlocking and other discontinuous features that are not considered in classical control theory. A method for calculating interlock conditions for particular operations from system safety assertions is proposed; it is similar to ordinary Z precondition calculation, but usually results in stronger preconditions. The specification is presented as a partially complete framework that can be edited and filled in with the specific features of a particular control system. Our system is large but the specification is concise. It is built up from components, subsystems, conditions and modes that are developed separately, but also accounts for behaviors that emerge at the system level. The specification illustrates several useful idioms of the Z notation, and demonstrates that an object- oriented specification style can be expressed in ordinary Z. [ABSTRACT FROM AUTHOR]

PVS is the most recent in a series of verification systems developed at SRI. Its design was strongly influenced, and later refined, by our experiences in developing formal specifications and mechanically checked verifications for the fault-tolerant architecture, algorithms, and implementations of a model "reliable computing platform" (RCP) for life-critical digital flight-control applications, and by a collaborative project to formally verify the design of a commercial avionics processor called AAMP5. Several of the formal specifications and verifications performed in support of RCP and AAMPS are individually of considerable complexity and difficulty. But in order to contribute to the overall goal, it has often been necessary to modify completed verifications to accommodate changed assumptions or requirements, and people other than the original developer have often needed to understand, review, build on, modify, or extract part of an intricate verification. In this paper, we outline the verifications performed, present the lessons learned, and describe some of the design decisions taken in PVS to better support these large, difficult, iterative, and collaborative verifications. [ABSTRACT FROM AUTHOR]

How should iterators be abstracted and encapsulated in modern imperative languages? We consider the combined impact of several factors on this question: the need for a common interface model for user defined iterator abstractions, the importance of formal methods in specifying such a model, and problems involved in modular correctness proofs of iterator implementations and clients. A series of iterator designs illustrates the advantages of the swapping paradigm over the traditional copying paradigm. Specifically, swapping based designs admit more efficient implementations while offering relatively straight- forward formal specifications and the potential for modular reasoning about program behavior. The final proposed design schema is a common interface model for an iterator for any generic collection. [ABSTRACT FROM AUTHOR]

Formal methods have had little impact on software engineering practice, despite the fact that most software engineering practitioners readily acknowledge the potential benefits to be gained from the mathematical modeling involved. One reason is that existing modeling techniques tend not to address basic software engineering concerns. In particular, while considerable attention has been paid to the construction of formal models, less attractive maintenance issues have largely been ignored. The purpose of this paper is to clarify those issues and ex- amine the underlying requirements for change support. The discussion is illustrated with a description of a change technique and tool developed for the formal notation LOTOS. This work was undertaken as part of the SCAFFOLD project, which was concerned with providing broad support for the construction and analysis of formal specifications of concurrent systems. Most of the discussion is applicable to other process-oriented notations such as CCS and CSP. [ABSTRACT FROM AUTHOR]

We address the problem of formally analyzing the properties of real-time systems. We propose a method based on modeling the system as a timed Petri net and on specifying its properties in TRIO, an extension of temporal logic suitable for dealing explicitly with time and for measuring it. Timed Petri nets are axiomatized in terms of TRIO, so that their properties can be derived as theorems in the same spirit as the classical Hoare method allows one to prove properties of programs coded in a Abstract- Measurement of software reliability by life testing involves executing the software on large numbers of test cases and recording the results. The number of failures observed is used to bound the failure probability even if the number of failures observed is zero. Typical analyses assume that all failures that occur are observed, but, in practice, failures occur without being observed. In this paper, we examine the effect of imperfect error detection, i.e., the situation in which a failure of the software may not be observed. If a conventional analysis associated with life testing is used, the confidence in the bound on the failure probability is optimistic. Our results show that imperfect error detection does not necessarily limit the ability of life testing to bound the probability of failure to the very low values required in critical systems. However, we show that the confidence level associated with a bound on failure probability cannot necessarily be made as high as desired, unless very strong assumptions are made about the error detection mechanism. Such assumptions are unlikely to be met in practice, and so life testing is likely to be useful only for situations in which very high confidence levels are not required. Pascal-like language. The method is also illustrated through an example. [ABSTRACT FROM AUTHOR]

This work is about the formal specification of transaction-based, interactive information systems. A transaction is a task that the user can execute independently, and the system can be defined as a partially ordered set of transactions. The general framework is the transformational paradigm, based on the classical Waterfall development model [28]. The stages are systems analysis, software specification, design, and implementation. In this work, the systems analysis and software specification stages are covered. An informal, transaction-oriented method for systems analysis is proposed. The resulting system specification involves two parts: a high-level specification of each transaction and a formal specification of the system's control flow, i.e., the order of execution of the transactions. The system's control flow is expressed in a formal language describing concurrent regular expressions built on transaction names. The detailed specification and design of a transaction was covered in an earlier article [3]. At the software specification stage, some operational requirements, such as connect/disconnect transactions and the application of the all-or-nothing principle, are added to the system specification. Then a serial product automaton (SPA) is used to transform the concurrent expression into a single regular expression. This result is proven to be consistent with the system specification. [ABSTRACT FROM AUTHOR]

We describe a rely and guarantee method for Timed CSP, by which we specify the behavior of a component belonging to a composite system in terms of what it guarantees to its neighbors and what it relies on from them. We illustrate the method by presenting an overview of our specification of POTS (Plain Old Telephone Service) together with part of a design which provably satisfies this specification. The specification and design deal with safety, liveness, and troublesome race conditions. [ABSTRACT FROM AUTHOR]

We present the formal derivation of an implementation of the I/O subsystem portion of an existing operating system. The I/O subsystem is responsible for allocating I/O resources (e.g., tapes, disks, I/O channels) in response to requests from user processes. The derivation employs the UNITY methodology [2], which nicely captures the concurrent interaction of the I/O subsystem with its environment. The verified resource allocation algorithm that results from the derivation has been used as part of a high-level design by software engineers implementing the I/O subsystem. As the largest application to date of the UNITY methodology, the derivation illustrates a number of techniques for organizing large specifications and proofs. [ABSTRACT FROM AUTHOR]

In this paper, we demonstrate how model checking can be used to verify safety properties for event-driven systems. SCR tabular requirements describe required system behavior in a format that is intuitive, easy to read, and scalable to large systems (e.g., the software requirements for the A7 aircraft). Model checking of temporal logics has been established as a sound technique for verifying properties of hardware systems. We have developed an automated technique for formalizing the semiformal SCR requirements and for transforming the resultant formal specification onto a finite structure that a model checker can analyze. This technique was effective in uncovering violations of system invariants in both an automobile cruise control system and a water-level monitoring system. [ABSTRACT FROM AUTHOR]

In this paper we describe SPECIFIER, an interactive system which derives formal specifications of data types and programs from their informal descriptions. We view the process of deriving formal specifications as a problem-solving process. The system uses common problem-solving techniques such as the use of schemas, analogy, and difference-based reasoning, to derive formal specifications. If an informal description is a commonly occurring operation for which the system has a schema, then the formal specification is derived by instantiating the schema. If there is no such schema, SPECIFIER tries to find a previously solved problem which is analogous to the current problem. If the problem found is in direct analogy with the current problem, it applies an analogy mapping to obtain a formal specification. On the other hand, if the analogy found is only approximate, it solves the directly analogous part of the problem by analogy, and then performs difference-based reasoning using the remaining (unmatched) parts to transform the formal specification obtained by analogy to a formal specification for the entire original problem. [ABSTRACT FROM AUTHOR]

The only built-in mechanism for data movement in most modern programming languages is the assignment statement for copying the value of one variable to another. In the context of reusable software components, this reliance on copying leads to two classes of difficulties: components whose implementations are inherently inefficient, and client programs that are hard to reason about. A powerful substitute for copying as the primary data movement primitive is a swapping mechanism that exchanges the values of two variables. Reusable components and client programs designed with a "swapping style" of programming have many advantages over designs based on the traditional "copying style," including improved execution efficiency, higher reliability, and enhanced reusability. [ABSTRACT FROM AUTHOR]

Miró is a set of languages and tools that support visual specification of file system security. We present two visual languages: the instance language, which allows specification of file system access, and the constraint language, which allows specification of security policies. We also describe tools we have implemented and give examples of how our languages can be applied to real security specification problems. [ABSTRACT FROM AUTHOR]

This paper describes the Penelope verification editor and its formal basis. Penelope is a prototype system for the interactive development and verification of programs that are written in a rich sub- set of sequential Ada. Because it generates verification conditions incrementally, Penelope can be used to develop a program and its correctness proof in concert. If an already-verified program is modified, one can attempt to prove the modified version by replaying and modifying the original sequence of proof steps. Verification conditions are generated by predicate transformers whose logical soundness can be proven by establishing a precise formal connection between predicate transformation and denotational definitions in the style of continuation semantics. Penelope's specification language, Larch/Ada, belongs to the family of Larch interface languages. It scales up properly, in the sense that we can demonstrate the soundness of decomposing an implementation hierarchically and reasoning locally about the implementation of each node in the hierarchy. [ABSTRACT FROM AUTHOR]

An important principle of building trustworthy systems is to rigorously analyze the critical requirements early in the development process, even before starting system design. Existing proof methods for systems of communicating processes focus on the bottom-up composition of component-level specifications into system-level specifications. Trustworthy system development requires, instead, the top-down derivation of component requirements from the critical system requirements. This paper describes a formal method for decomposing the requirements of a system into requirements of its component processes and a minimal, possibly empty, set of synchronization requirements. The Trace Model of Hoare's Communicating Sequential Processes (CSP) is the basis for the formal method. We apply the method to an abstract voice transmitter and describe the role that the EHDM verification system plays in the transmitter's decomposition. In combination with other verification techniques, we expect that the method defined here will promote the development of more trustworthy systems. [ABSTRACT FROM AUTHOR]

Formal specification methods are being used to improve the quality of written specifications, and particularly to eliminate errors at an early stage of software development. The detection of errors in a specification generally requires that we compare the specification against some loosely defined "real-world'' concepts. In this correspondence we introduce a new criterion for evaluating the quality of a model-oriented specification and explain the problems associated with specifications which do not meet this criterion. These problems are particularly troublesome when reusable software components are being specified or when a bottom-up implementation strategy is being used. [ABSTRACT FROM AUTHOR]

This paper shows how design time testing may be used in conjunction with formal specification. Emphasis is placed upon the benefits of using an executable specification language OBJ, a design controlled by requirements specification and adherence to the "regularity" and "uniformity" hypotheses in dynamic validation. Such an approach offers positive benefits by providing early design validation and a controlled, disciplined design process. [ABSTRACT FROM AUTHOR]

Sixty percent of the software costs associated with the design, development, and implementation of computer systems occurs in the maintenance phase. A significant reduction in the maintenance costs can be realized with a design for change philosophy integrated into the engineering life cycle. By carefully identifying the expected changes to a system and rigorously applying the concepts of information hiding and abstraction of interfaces, the changeable aspects of a system can be isolated. In 1978, a Software Cost Reduction program was initiated whose goal was to apply these modern design and documentation principles to the development of large systems. The results of this effort have been documented in several research papers published by Parnas and associates. This paper extends that approach by updating the methodology based upon lessons learned during the application of the concepts to the development of a computer-based training system. An engineering life cycle which provides more visibility to maintenance concerns is described and the lessons learned during its implementation are discussed. Finally, a summary provides our impressions of the methodology and its potential to reduce system maintenance costs. [ABSTRACT FROM AUTHOR]

This paper presents a formalization of the WEE standard for binary floating-point arithmetic in the set-theoretic specification language Z. The formal specification is refined into four sequential components, which unpack the operands, perform the arithmetic, and pack and round the result. This refinement follows proven rules and so demonstrates a mathematically rigorous method of program development. in the course of the proofs, useful internal representations of floating-point numbers are specified. The procedures which are presented here form the basis for the floating-point unit of the inmos EMS T800 transputer. [ABSTRACT FROM AUTHOR]

Formal program construction by transformations is a method of software development in which a program is derived from a formal problem specification by manageable, controlled transformation steps which guarantee that the final product meets the initial specification. This methodology has been investigated in the Munich project CIP (computer-aided, intuition-guided programming). The research includes the design of a wide-spectrum language specifically tailored to the needs of transformational programming, the construction of a transformation system to support the methodology, and the study of transformation rules and other methodological issues. Particular emphasis has been laid on developing a sound theoretical basis for the overall approach. [ABSTRACT FROM AUTHOR]

PROSPEC is a software environment for designing and verifying communication protocols. It integrates several tools that implement methods for protocol verification and construction (e.g., fair reachability analysis, multiphase construction and protocol projection). The system provides a unified graphical interface to facilitate the application of these methods and creates an interactive environment for specifying, verifying and designing communication protocols. PROSPEC was used successfully to design and verify versions of BSC, X.21, X.25, and Telnet document transfer protocols. [ABSTRACT FROM AUTHOR]

RTAG is a language based on an attribute grammar notation for specifying protocols. Its main design goals are: 1) to support concise and easily understood expression of complex real-world protocols, and 2) to serve as the basis of a portable software system for automated protocol implementation. This paper summarizes the RTAG language, gives examples of its use, sketches the algorithms used in generating implementations from these specifications, and describes a UNIX®-based automated implementation system for RTAG. [ABSTRACT FROM AUTHOR]

The use of formal specifications in software development allows the use of certain automated tools during the specification and software development process: Formal description techniques have been developed for the specification of communication protocols and services. This paper describes the partial automation of the protocol implementation process based on a formal specification of the protocol to be implemented. An implementation strategy and a related software structure for the implementation of state transition oriented specifications is presented. Its application is demonstrated with a much simplified Transpart protocol. The automated translation of specifications into implementation code in a high-level language is also discussed. A semiautomated implementation strategy explained which highlights several refinement steps, part of which are automated, which lead from a formal protocol specification to an Implementation. Experience with several lull implementations of the PSI Transport protocol is described. [ABSTRACT FROM AUTHOR]

Communication protocol testing can be done with a test architecture consisting of remote Lower Tester and local Upper Tester processes. For real protocols, tests can be designed based on the formal specification of the protocol which uses an extended finite state machine model. The specification is transformed into a simpler form consisting of normal form transitions. It can then be modeled by a control and a data flow graph. The graphs are decomposed into subtours and data flow functions, respectively. Tests are designed by considering parameter variations of the input primitives of each data flow function and determining the expected outputs. The methodology gives complete test coverage of all data flow functions and control paths in the specification. Functional fault models are proposed for functions that are not formally specified. [ABSTRACT FROM AUTHOR]

In carrying out SOC's Formal Development Method, one writes a specification of a system under design in the Ina Jo™ specification language and proves that the specification meets the requirements of the system. This paper develops an abstract machine model of what is specified by a level specification in an ma Jo specification. It describes the state as defined by the front matter, computations as defined by initial states and transforms, and invariants, criteria, and constraints as properties of computations. The paper then describes a number of formal design methods and the kinds of abstractions that they require. For each of these kinds of abstractions, there is a characteristic relationship between refinements that should be proved as one is carrying out the method. [ABSTRACT FROM AUTHOR]

This paper examines the application of two covert channel analysis techniques to a high level design for a real system, the Honeywell Secure Ada® Target (SAT). The techniques used were a version of the noninterference model of multilevel security due to Goguen and Meseguer and the shared resource matrix method of Kemmerer. Both techniques were applied to the Gypsy Abstract Model of the SAT. The paper discusses the application of the techniques and the nature of the covert channels discovered. The relative strengths and weaknesses of the two methods are discussed and criteria for an ideal covert channel tool are developed. [ABSTRACT FROM AUTHOR]

RT-ASLAN is a formal language for specifying real-time systems. It is an extension of the ASLAN specification language for sequential systems. Some of the features of the ASLAN language, such as constructs for writing procedural semantics in a nonprocedural logical language, are highlighted. The RT-ASLAN language supports specification of parallel real-time processes through arbitrary levels of abstraction; processes do not have to be specified to the same level of detail. Communicating processes use an interface process as an abstract data type representing shared information. From RT-ASLAN specifications, performance correctness conjectures are generated. These conjectures are logic statements whose proof guarantees the specification meets critical time bounds. A detailed example as well as a discussion of the advantages and disadvantages of formal specification and verification are included. [ABSTRACT FROM AUTHOR]

• Safety demonstration of software is required when developing safety systems. • Software fault tree analysis is one of the software safety analysis technique. • There are less studies on analyzing timing constraints for multi-cycled operations by software fault tree analysis mechanically. • This paper proposes a software fault tree analysis technique for software requirements written in NuSCR formal specification language. • The proposed technique constructs software fault trees and minimal cut-sets encompassing timing constraints of multi-cycles. Rigorous safety demonstration of software, as well as systems, is required when developing digital reactor protection systems in nuclear power plants. Various safety analysis techniques try to identify, analyze, and find remedies for potential hazards at each stage of software development life-cycle. This paper proposes a software fault tree analysis technique for software requirements written in the NuSCR formal specification language. The proposed method can mechanically construct software fault trees and calculate minimal cut-sets, encompassing timing constraints of multi-cycles, from NuSCR formal specifications. We also improved the fault tree construction and analysis tool into " NuFTA 2.0 " to cope with multi-cycled executions. The case study with a preliminary version of requirements specification for a Korean nuclear power plant in operation shows the proposed technique's effectiveness and applicability to other V&Vs such as simulation. [ABSTRACT FROM AUTHOR]

The authentication protocol for HTTP proposed in RFC 8120 has been model checked under different assumptions. Four security properties have been taken into account: (1) Key Secrecy Property (K-SEC), (2) Key Sharing Property (K-SHR), (3) Correspondence Property from a client point of view (C-CORR), and (4) Correspondence Property from a server point of view (S-CORR). In each assumption, we suppose that there exists an intruder that eavesdrops on the network and forges messages based on any pieces of information available. Under the assumption (a) that the cryptosystem used is perfect, the formal analysis concludes that the protocol is likely to enjoy K-SEC and K-SHR, but reveals that it enjoys neither C-CORR nor S-CORR. Under the assumption (b) that pseudo-random numbers generated by clients are leaked to the intruder, the results are the same. Under the assumption (c) that pseudo-random numbers generated by servers are leaked to the intruder, however, the protocol enjoys neither K-SEC nor K-SHR. To discover a realistic counterexample for K-SHR, a model checking experiment has been divided into multiple smaller ones. We then propose a revised version, which is likely to enjoy all four properties even under the assumption (c). [ABSTRACT FROM AUTHOR]

In the paper [1], Theorem 23 and Example 24 are incorrect. The corrected version is presented in this note. [ABSTRACT FROM AUTHOR]

We address the problem of how to reason about properties of knowledge transformations as they occur in distributed and decentralized interactions between large and complex artifacts, such as databases, web services, and ontologies. Based on the conceptual distinction between specifications of interactions and properties of knowledge transformations that follow from these interactions, we explore a novel mixture of process calculus and property inference by connecting interaction models with knowledge transformation rules. We aim at being generic in our exploration, hence our emphasis on abstract knowledge transformations, although we exemplify it using a lightweight specification language for interaction modeling (for which an executable peer-to-peer environment already exists) and provide a formal semantics for knowledge transformation rules using the theory of institutions. Consequently, our exploration is also an example of the gain obtained by linking current state-of-the-art distributed knowledge engineering based on web services and peer-based architectures with formal methods drawn from a long tradition in algebraic specification. [ABSTRACT FROM PUBLISHER]