基于场景分析的系统形式化模型生成方法

采用形式化方法对系统的安全性进行分析与验证,是构造可靠安全软件系统的一个重要途径。当前的形式化安全分析方法,面临着系统的形式化建模难的问题。以铁路车站联锁系统中基本进路建立为例,提出基于场景分析的系统形式化模型生成方法。该方法首先采用OCL前/后置条件分析法对UML时序场景作一致性分析,然后将UML时序图中对象交互的行为序列转换成FSP进程代数模型,进而得到系统的形式化模型。该方法为系统的形式化建模提供了新思路,从安全质量方面改善了安全苛求软件的设计与开发,丰厚了基于模型的软件形式化开发方法。     

Design and verification of fault tolerant systems with CSP

Summary By means of an example, we present a formal method based on CSP to design fault tolerant systems. This method combines algebraic and assertional techniques to achieve complete formal verification of the fault tolerant system's correctness properties. Verification steps are executed in parallel with top-down design, so that correctness proofs can be clearly structured and their completeness easily checked. In this way formal verification is applicable not only to small examples but to reasonably large systems. Jan Peleska was born in 1958 in Hamburg, received his Diploma in Mathematics from the University of Hamburg in 1981 and a Ph.D. in Mathematics in 1982. From 1981 to 1984 he worked in research and software development projects in the field of accoustics. Since 1984 he has been working with Philips and DST in Kiel in the field of distributed information systems. Peleska's current research interests include fault tolerant systems, distributed database systems and formal design and verification methods.     

A case study in the mechanical verification of fault tolerance

To date, there is little evidence that modular reasoning about fault-tolerant systems can simplify the verification process in practice. This question is studied using a prominent example from the fault tolerance literature: the problem of reliable broadcast in point-to-point networks subject to crash failures of processes. The experiences from this case study show how modular specification techniques and rigorous proof re-use can indeed help in such undertakings.     

Formal specification and compositional verification of an atomic broadcast protocol

We apply a formal method based on assertions to specify and verify an atomic broadcast protocol. The protocol is implemented by replicating a server process on all processors in a network. We show that the verification of the protocol can be done compositionally by using specifications in which timing is expressed by local clock values. First the requirements of the protocol are formally described. Next the underlying communication mechanism, the assumptions about local clocks, and the failure assumptions are axiomatized. Also the server process is represented by a formal specification. Then we verify that parallel execution of the server processes leads to the desired properties by proving that the conjunction of all server specifications and the axioms about the system implies the requirements of the protocol.     

Formal verification of the NASA runway safety monitor

The runway safety monitor (RSM) designed by Lockheed Martin is part of NASA’s effort to reduce aviation accidents. We developed a Petri net model of the RSM protocol and used the model checking functions of our tool (stochastic and model checking analyzer for reliability and timing) SMART (Stochestic and model checking analyses for seliability and tunnig) to investigate a number of safety properties for the RSM. To mitigate the impact of state-space explosion, we built a highly discretized model of the system, obtained by partitioning the monitored runway zone into a grid of smaller volumes and by considering scenarios involving only two aircraft. The model also assumes that there are no communication failures, such as bad input from radar or lack of incoming data, thus it relies on a consistent view of reality by all participants. In spite of these simplifications, we were able to expose potential problems in the conceptual design of RSM. Our findings were forwarded to the design engineers, who undertook corrective action. Additionally, the results stress the efficiency attained by the new model checking algorithms implemented in SMART, and demonstrate their applicability to real-world systems. Attempts to verify RSM with similar NuSMV and SPIN models have failed due to excessive memory consumption. Work supported in part by the National Aeronautics and Space Administration under grant NAG-1-02095 and by the National Science Foundation under grants CCR-0219745 and ACI-0203971.     

Formal verification of static software models in MDE: A systematic review

ContextModel-driven Engineering (MDE) promotes the utilization of models as primary artifacts in all software engineering activities. Therefore, mechanisms to ensure model correctness become crucial, specially when applying MDE to the development of software, where software is the result of a chain of (semi)automatic model transformations that refine initial abstract models to lower level ones from which the final code is eventually generated. Clearly, in this context, an error in the model/s is propagated to the code endangering the soundness of the resulting software. Formal verification of software models is a promising approach that advocates the employment of formal methods to achieve model correctness, and it has received a considerable amount of attention in the last few years.ObjectiveThe objective of this paper is to analyze the state of the art in the field of formal verification of models, restricting the analysis to those approaches applied over static software models complemented or not with constraints expressed in textual languages, typically the Object Constraint Language (OCL).MethodWe have conducted a Systematic Literature Review (SLR) of the published works in this field, describing their main characteristics.ResultsThe study is based on a set of 48 resources that have been grouped in 18 different approaches according to their affinity. For each of them we have analyzed, among other issues, the formalism used, the support given to OCL, the correctness properties addressed or the feedback yielded by the verification process.ConclusionsOne of the most important conclusions obtained is that current model verification approaches are strongly influenced by the support given to OCL. Another important finding is that in general, current verification tools present important flaws like the lack of integration into the model designer tool chain or the lack of efficiency when verifying large, real-life models.     

Formal verification of the Merchant Registration phase of the SET protocol

This paper describes the formal verification of the Merchant Registration phase of the Secure Electronic Transactions (SET) protocol, a realistic electronic transaction security protocol which is used to protect the secrecy of online purchases. A number of concepts, notations, functions, predicates, assumptions and rules are introduced. We describe the knowledge of all legal participants, and a malicious spy, to assess the security of the sub-protocol. Avoiding search in a large state space, the method converges very quickly. We implemented our method in the Isabelle/Isar automated reasoning environment, therefore the whole verification process can be executed mechanically and efficiently.     

Probabilistic analysis on mesh network fault tolerance

Mesh networks are among the most important interconnection network topologies for large multicomputer systems. Mesh networks perform poorly in tolerating faults in the view of worst-case analysis. On the other hand, such worst cases occur very rarely in realistic situations. In this paper, we study the fault tolerance of 2-D and 3-D mesh networks under a more realistic model in which each network node has an independent failure probability. We first observe that if the node failure probability is fixed, then the connectivity probability of these mesh networks can be arbitrarily small when the network size is sufficiently large. Thus, it is practically important for multicomputer system manufacture to determine the upper bound for node failure probability when the probability of network connectivity and the network size are given. We develop a novel technique to formally derive lower bounds on the connectivity probability for 2-D and 3-D mesh networks. Our study shows that these mesh networks of practical size can tolerate a large number of faulty nodes thus are reliable enough for multicomputer systems. For example, it is formally proved that as long as the node failure probability is bounded by 0.5%$0.5\%$, a 3-D mesh network of up to a million nodes remains connected with a probability larger than 99%$99\%$.     

End-to-end fault tolerance

In this review we survey both standard fault tolerance theory and Kitaev’s model for quantum computation, and demonstrate how they can be combined to yield quantitative results that reveal the interplay between the two. This analysis establishes a methodology allowing one to quantitatively determine design parameters for quantum computers, the values of which ensure that an overall computation yields a correct final result with some prescribed probability of success, as opposed to merely ensuring that the desired final quantum state is obtained. As an example, we explicitly calculate the number of levels of error correction concatenation needed to achieve a correct final result with some prescribed success probability. This methodology allows one to determine parameters required in order to achieve the correct final result for the quantum computation, as opposed to merely ensuring that the desired final quantum state is produced.      

Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL

We present a formalization and a formal total correctness proof of a MiniSAT-like SAT solver within the system Isabelle/HOL. The solver is based on the DPLL procedure and employs most state-of-the-art SAT solving techniques, including the conflict-guided backjumping, clause learning, and the two-watched unit propagation scheme. A shallow embedding into Isabelle/HOL is used and the solver is expressed as a set of recursive HOL functions. Based on this specification, the Isabelle’s built-in code generator can be used to generate executable code in several supported functional languages (Haskell, SML, and OCaml). The SAT solver implemented in this way is, to our knowledge, the first fully formally and mechanically verified modern SAT solver.     

A study of fault tolerance in star graph

The bounds on f(n,k), the number of faulty nodes to make every (n−k)-dimensional substar Sn−k in an n-dimensional star network Sn, have been derived. The exact value for f(n,k) is determined when n is prime and k=2, or when n−2?k?n. For 2<k<n−2, a general method is presented to derive a set of faulty nodes which damage all Sn−k's in Sn.     

Fault tolerance in co-evolutionary communication of EHW modules

Evolvable Hardware (EHW) is a new concept that applies evolutionary algorithms to hardware design. Based on previous work on co-evolutionary communication of EHW modules, this paper investigates the new feature of fault tolerance for this model. A fault model is built for the communication line between EHW modules. The experiment demonstrated in the presentation is the simulation of injecting stuck/bridging faults into an EHW-based serial adder that has been previously developed. The outcomes imply an outstanding feature of fault tolerance in this system with 100% fault coverage, which paves the way for bio-inspired approaches to fault tolerant design instead of the classic ones.     

Security enhancement for digital signature schemes with fault tolerance in RSA

Digital signature schemes with fault tolerance make it possible for error detections and corrections during the processes of data computations and transmissions. Recently, Zhang, in 1999, and Lee and Tsai, in 2003, have respectively proposed two efficient fault-tolerant schemes based on the RSA cryptosystem. Both of them can efficiently check the sender’s identity and keep the confidentiality of the transmitted document. Furthermore, they can detect the errors and correct them. However, these schemes have a common weakness in security, that is, different messages may easily be computed that have the same signature. Thus, a valid signature could be reused in another document. This severely violates the principles of digital signature. In this paper, we shall show that this security flaw existed in the two perviously proposed schemes and conclude that the security flaw may occur in other fault-tolerant public key cryptosystems that are similar to these schemes. Furthermore, we will improve Zhang’s and Lee and Tsai’s schemes to eliminate the drawbacks.     

Algorithm-based fault tolerance applied to high performance computing

We present a new approach to fault tolerance for High Performance Computing system. Our approach is based on a careful adaptation of the Algorithm-Based Fault Tolerance technique [K. Huang, J. Abraham, Algorithm-based fault tolerance for matrix operations, IEEE Transactions on Computers (Spec. Issue Reliable & Fault-Tolerant Comp.) 33 (1984) 518–528] to the need of parallel distributed computation. We obtain a strongly scalable mechanism for fault tolerance. We can also detect and correct errors (bit-flip) on the fly of a computation. To assess the viability of our approach, we have developed a fault-tolerant matrix–matrix multiplication subroutine and we propose some models to predict its running time. Our parallel fault-tolerant matrix–matrix multiplication scores 1.4 TFLOPS on 484 processors (cluster jacquard.nersc.gov) and returns a correct result while one process failure has happened. This represents 65% of the machine peak efficiency and less than 12% overhead with respect to the fastest failure-free implementation. We predict (and have observed) that, as we increase the processor count, the overhead of the fault tolerance drops significantly.     

Scenario-based verification in presence of variability using a synchronous approach

This paper presents a new model of scenarios, dedicated to the specification and verification of system be- haviours in the context of software product lines （SPL）. We draw our inspiration from some techniques that are mostly used in the hardware community, and we show how they could be applied to the verification of software components. We point out the benefits of synchronous languages and mod- els to bridge the gap between both worlds.     

Generalised multi-pattern-based verification of programs with linear linked structures

The paper deals with the problem of automatic verification of programs working with extended linear linked dynamic data structures, in particular, pattern-based verification is considered. In this approach, one can abstract memory configurations by abstracting away the exact number of adjacent occurrences of certain memory patterns. With respect to the previous work on the subject the method presented in the paper has been extended to be able to handle multiple patterns, which allows for verification of programs working with more types of structures and/or with structures with irregular shapes. The experimental results obtained from a prototype implementation of the method show that the method is very competitive and offers a big potential for future extensions.     

Putting it all together – Formal verification of the VAMP

In the verified architecture microprocessor (VAMP) project we have designed, functionally verified, and synthesized a processor with full DLX instruction set, delayed branch, Tomasulo scheduler, maskable nested precise interrupts, pipelined fully IEEE compatible dual precision floating point unit with variable latency, and separate instruction and data caches. The verification has been carried out in the theorem proving system PVS. The processor has been implemented on a Xilinx FPGA. A shorter version of this article with the title “Instantiating uninterpreted functional units and memory system: functional verification of the VAMP” appeared in [8]. The work reported here was done while all the authors were with Saarland University.     

Fault tolerance in cellular automata at high fault rates

A commonly used model for fault-tolerant computation is that of cellular automata. The essential difficulty of fault-tolerant computation is present in the special case of simply remembering a bit in the presence of faults, and that is the case we treat in this paper. We are concerned with the degree (the number of neighboring cells on which the state transition function depends) needed to achieve fault tolerance when the fault rate is high (nearly 1/2). We consider both the traditional transient fault model (where faults occur independently in time and space) and a recently introduced combined fault model which also includes manufacturing faults (which occur independently in space, but which affect cells for all time). We also consider both a purely probabilistic fault model (in which the states of cells are perturbed at exactly the fault rate) and an adversarial model (in which the occurrence of a fault gives control of the state to an omniscient adversary). We show that there are cellular automata that can tolerate a fault rate 1/2−ξ (with ξ>0) with degree O((1/ξ²)log(1/ξ)), even with adversarial combined faults. The simplest such automata are based on infinite regular trees, but our results also apply to other structures (such as hyperbolic tessellations) that contain infinite regular trees. We also obtain a lower bound of Ω(1/ξ²), even with only purely probabilistic transient faults.     

A kind of conditional fault tolerance of alternating group graphs

A vertex subset F is a k-restricted vertex-cut of a connected graph G if G−F is disconnected and every vertex in G−F has at least k good neighbors in G−F. The cardinality of the minimum k-restricted vertex-cut of G is the k-restricted connectivity of G, denoted by κk(G). This parameter measures a kind of conditional fault tolerance of networks. In this paper, we show that for the n-dimensional alternating group graph AGn, κ²(AG₄)=4 and κ²(AGn)=6n−18 for n?5.     

Formal verification of software source code through semi-automatic modeling

We describe the experience of modeling and formally verifying a software cache algorithm using the model checker RuleBase. Contrary to prevailing wisdom, we used a highly detailed model created directly from the C code itself, rather than a high-level abstract model.