Formal Verification of a Consensus Algorithm in the Heard-Of ModelReal-Time Embedded Systems Using VDM

Distributed algorithms are subtle and error-prone. Still, very few of them have been formally verified, most algorithm designers only giving rough and informal sketches of proofs. We believe that this unsatisfactory situation is due to a scalability problem of current formal methods and that a simpler model is needed to reason about distributed algorithms. We consider formal verification of algorithms expressed in the Heard-Of model recently introduced by Charron-Bost and Schiper. As a concrete case study, we report on the formal verification of a non-trivial Consensus algorithm using the proof assistant Isabelle/HOL.     

对称密码算法专用描述语言的函数设计

对称密码算法专用描述语言(svLSCa)以自然的类似专业语言的思维方式描述算法的设计思想。在密码算 法设计中,对于已经证明安全性高的、性能良好的密码构件会重复采用,比如s变换、P置换等。在分析大量公开密码 算法设计特点和规律的基础上,在svLSCa语法中增加函数机制。详细给出了svLSCa中函数的定义、调用以及实 现的关键技术。并以AEC为例,说明函数在算法描述的应用。实践表明利用SDLSCA中函数的功能,可以大大简化 算法描述,提高算法描述的利用率和效率。     

Application of a transformational software development methodology to VLSI design

Like software development, VLSI design can be modeled as a series of transformations leading from a high-level formal specification to a concrete implementation. Automating such transformations offers a way to improve the correctness of the design process while reducing its cost. This paper addresses the portion of the design process that converts abstract algorithms into functional-level circuits (collections of primitive computational elements and their interconnections). By defining an isomorphism between such circuits and a restricted subset of programs, we can use source-to-source program transformations to map algorithms into circuits. The paper presents example transformations for allocating operations to components, making communication paths explicit, and designing sequential control mechanisms. A prototype implementation has successfully rederived much of the design of a published VLSI graphics display processor.     

SLAN-4?A Software Specification and Design Language

SLAN-4 (``Software Language-4') was developed to meet the need for a formal tool for specifying and designing large software systems. It provides language constructs for algebraic and axiomatic specifications and also pseudocode constructs for the design step. A major design goal was to ease subsequent refinements of a (given) specification. The design can start with a very informal specification, which can be implemented later using lower level concepts. This paper gives an overview of the SLAN-4 syntax and semantics. It concentrates on the most important aspects of: ? abstract data types, ? algebraic specification of abstract data types, and ? axiomatic specification of modules. Because the pseudocode part of SLAN-4 consists mainly of control structures similar to those in modern high-level programming languages, this element of the language is not separately described. The paper includes an example of how to use SLAN-4, and also the experiences gained in using the language to formally specify a real-world software product of about 18 000 lines of code written in an IBM internal high-level language.     

Invariant-based verification of a distributed deadlock detectionalgorithm

It is argued that most previous proposals for distributed deadlock detection are incorrect because they have used informal/intuitive arguments to prove the correctness of their algorithms. Informal and intuitive arguments are prone to errors because of the highly complex nature of distributed deadlock detection/resolution algorithms. The priority-based probe algorithm for distributed deadlock detection and resolution of A.L. Choudhary et al. (1989) is corrected, and it is formally proven that the modified algorithm is correct (i.e., that it does detect all deadlocks and does not report phantom deadlocks). The proof technique is novel in that the authors first abstract the properties of the deadlock detection and resolution algorithm by invariants, and then show that the invariants imply the desired correctness of the algorithm     

A formal approach to scenario integration

The scenario technique is an interesting approach for eliciting requirements. A formal approach to scenario generation has made it even more attractive. The next logical step is to integrate several scenarios into one single, consistent, specification. In this work, a mixed approach, involving formal and informal steps is proposed for performing this task. The system's formal specification is expressed as a finite state machine. The specifications of two interacting scenarios are integrated in a procedure involving formal and informal steps. Then several algorithms based on the properties of the model, are applied to detect three classes of errors: mistakes made by the analyst during the informal steps of the integration, inconsistencies between the scenarios, and incompleteness of both scenarios. Each algorithm detects the corresponding specification errors and in addition, suggests the corrections to apply. The formal techniques applied in this work could be the basis of a CASE tool for scenario‐based requirements engineering.     

Playing with state-based models for designing better algorithms

State-based models provide a very convenient framework for analyzing, verifying, validating and designing sequential as well as concurrent or distributed algorithms. Each state-based model is considered as an abstraction, which is more or less close to the target algorithmic entity. The problem is then to organize the relationship between an initial abstract state-based model expressing requirements and a final concrete state-based model expressing a structured algorithmic state-based model. A simulation (or refinement) relation between two state-based models allows to structure these models from an abstract view to a concrete view. Moreover, state-based models can be extended by assertion languages for expressing correctness properties as pre/post specification, safety properties or even temporal properties. In this work, we review state-based models and play scores for verifying and designing concurrent or distributed algorithms. We choose the Event-B modeling language for expressing state-based models and we show how we can play Event-B scores using Rodin and methodological elements to guarantee that the resulting algorithm is correct with respect to initial requirements. First, we show how annotation-based verification can be handled in the Event-B modeling language and we propose an extension to handle the verification of concurrent programs. In a second step, we show how important is the concept of refinement and how it can be used to found a methodology for designing concurrent programs using the coordination paradigm.     

Dynamic verification of C++ generic algorithms

Dynamic verification is a new approach to formal verification, applicable to generic algorithms such as those found in the Standard Template Library (STL, part of the Draft ANSI/ISO C++ Standard Library). Using behavioral abstraction and symbolic execution techniques, verifications are carried out at an abstract level such that the results can be used in a variety of instances of the generic algorithms without repeating the proofs. This is achieved by substituting for type parameters of generic algorithms special data types that model generic concepts by accepting symbolic inputs and deducing outputs using inference methods. By itself, this symbolic execution technique supports testing of programs with symbolic values at an abstract level. For formal verification one also needs to generate multiple program execution paths and use assertions (to handle while loops, for example), but the authors show how this can be achieved via directives to a conventional debugger program and an analysis database. The assertions must still be supplied, but they can be packaged separately and evaluated as needed by appropriate transfers of control orchestrated via the debugger. Unlike all previous verification methods, the dynamic verification method thus works without having to transform source code or process it with special interpreters. They include an example of the formal verification of an STL generic algorithm     

Formal models for user interface design artefacts

There are many different ways of building software applications and of tackling the problems of understanding the system to be built, designing that system and finally implementing the design. One approach is to use formal methods, which we can generalise as meaning we follow a process which uses some formal language to specify the behaviour of the intended system, techniques such as theorem proving or model-checking to ensure the specification is valid (i.e., meets the requirements and has been shown, perhaps by proof or other means of inspection, to have the properties the client requires of it) and a refinement process to transform the specification into an implementation. Conversely, the approach we take may be less structured and rely on informal techniques. The design stage may involve jotting down ideas on paper, brainstorming with users etc. We may use prototyping to transform these ideas into working software and get users to test the implementation to find problems. Formal methods have been shown to be beneficial in describing the functionality of systems, what we may call application logic, and underlying system behaviour. Informal techniques, however, have also been shown to be useful in the design of the user interface to systems. Given that both styles of development are beneficial to different parts of the system we would like to be able to use both approaches in one integrated software development process. Their differences, however, make this a challenging objective. In this paper we describe models and techniques which allow us to incorporate informal design artefacts into a formal software development process.     

面向应用的Web服务组合设计和验证框架

针对Web服务组合设计规范缺乏形式化的语义和验证方法的问题,提出了一个自顶向下的Web服务设计和验证的框架-iFrame4WS。在iFrame4WS中,将Web服务组合的设计方案划分为描述层、抽象层和执行层,并通过抽象层的形式化模型和形式化验证来检查Web服务组合的正确性。     

Development of a class of distributed termination detectionalgorithms

Accessing and updating information in a self organizing data structure in a distributed environment requires execution of various distributed algorithms. Design of such algorithms is often facilitated by the use of a distributed termination detection algorithm superimposed on top of another distributed algorithm. The problem of distributed termination detection is considered, and message counting is introduced as an effective technique in designing such algorithms. A class of efficient algorithms, based on the idea of message counting, for this problem is presented. After termination has occurred, it is detected within a small number of message communications. These algorithms do not require the FIFO (first in, first out) property for the communication lines. Assumptions regarding the connectivity of the processes are simple. The algorithms are incrementally developed, i.e. a succession of algorithms leading to the final algorithms is presented