Mechanical verification of the IEEE 1394a root contention protocol using Uppaal2k

This paper reports on the mechanical verification of the IEEE 1394 root contention protocol. This is an industrial leader election protocol, in which timing parameters play an essential role. A manual verification of this protocol using I/O automata has been published in [24]. We improve the communication model presented in that paper. Using the Uppaal2k tool, we investigate the timing constraints on the parameters which are necessary and sufficient for correct protocol operation: by analyzing large numbers of protocol instances with different parameter values, we derive the required timing constraints. We explore the use of model checking in combination with stepwise abstraction. That is, we show that the implementation automaton correctly implements the specification via several intermediate automata, using Uppaal to prove the trace inclusion in each step. Published online: 18 July 2001     

Uppaal到PVS的时间自动机翻译器

Uppaal是一种对实时系统模型进行建模和验证的工具,PVS（Prototype Verification System）是开发和分析形式化规格说明的原型证明系统。介绍了Uppaal2PVS翻译器的设计与实现,给出了一种将用Uppaal生成的时间自动机规格说明翻译成PVS文件的方法,从而将模型检查问题转换成了定理证明问题,解决了潜在的状态空间爆炸问题。最后给出了一个实例。     

Uncovering ISO ROSE protocol errors using Estelle

One of the main objectives of ISO in developing FDTs is that protocol specified in them can be verified. However, standardized FDTs have been designed largely for specification purpose; success of using them for protocol verification has been rarely reported. We have developed a technique of translating Estelle specifications into Numerical Petri nets, which can then be verified by a proven automated verification tool, PROTEAN. The merits of our approach are that specifications are fully based on standard Estelle, and dynamic behaviours of an Estelle specification can be handled. In this paper, we present a success story of using Estelle and the techniques we have developed to uncover ISO ROSE protocol errors. We find that Estelle is an FDT capable of analysing and verifying real protocols and it is therefore important to the development of ISO protocol standards.     

Verifying Communication Protocols Using Live Sequence Chart Specifications

The need for a formal verification process in System on Chip (SoC) design and Intellectual Property (IP) integration has been recognized and investigated significantly in the past. A major drawback is the lack of a suitable specification language against which definitive and efficient verification of inter-core communication can be performed to prove compliance of an IP block against the protocol specification. Previous research has yielded positive results of verifying systems against the graphical language of Live Sequence Charts (LSCs) but has identified key limitations of the process that arise from the lack of support for important constructs of LSCs such as Kleene stars, subcharts, and hierarchical charts. In this paper we further investigate the use of LSCs as a specification language and show how it can be formally translated to automata suitable for input to a model checker for automatic verification of the system under test. We present the translation for subcharts, Kleene stars, and hierarchical charts that are essential for protocol specification and have not been translated to automata before. Further, we successfully translate the BVCI protocol (point to point communication protocol) specification from LSC to an automaton and present a case study of verifying models using the resulting automaton.     

Modeling selected real-time database concurrency control protocols in Uppaal

Real-time database management systems (RTDBMS) are recently subject of an intensive research. Model checking algorithms and verification tools are of great concern as well. In this paper, we show some possibilities of using a verification tool Uppaal on some variants of pessimistic and optimistic concurrency control protocols used in real-time database management systems. We present some possible models of such protocols expressed as nets of timed automata, which are a modeling language of Uppaal. M. Kot acknowledges the support by the Czech Ministry of Education, Grant No. 1M0567.     

Specification and Verification of Communication Protocols in AFFIRM Using State Transition Models

It is becoming increasingly important that communication protocols be formally specified and verified. This paper describes a particular approach–the state transition model–using a collection of mechanically supported specification and verification tools incorporated in a running system called AFFIRM. Although developed for the specification of abstract data types and the verification of their properties, the formalism embodied in AFFIRM can also express the concepts underlying state transition machines. Such models easily express most of the events occurring in protocol systems, including those of the users, their agent processes, and the communication channels. The paper reviews the basic concepts of state transition models and the AFFIRM formalism and methodology and describes their union. A detailed example, the alternating bit protocol, illustrates varous properties of interest for specification and verification. Other examples explored using this formalism are briefly described and the accumulated experience is discussed.     

A Tool For Specification And Verification Of Epistemic Properties In Interpreted Systems

We present a compiler that translates a multi-agent systems specification given in the formalism of Interpreted Systems into an SMV program. We show how an SMV model checker can be coupled with a Kripke model editor (Akka) to allow for the mechanical verification of epistemic properties of multi-agent systems. We apply this methodology to the verification of a communication protocol — the dining cryptographers.     

Compositional verification of real-time systems using Ecdar

We present a specification theory for timed systems implemented in the Ecdar tool. We illustrate the operations of the specification theory on a running example, showing the models and verification checks. To demonstrate the power of the compositional verification, we perform an in depth case study of a leader election protocol; Modeling it in Ecdar as Timed input/output automata Specifications and performing both monolithic and compositional verification of two interesting properties on it. We compare the execution time of the compositional to the classical verification showing a huge difference in favor of compositional verification.     

How to stop time stopping

Zeno-timelocks constitute a challenge for the formal verification of timed automata: they are difficult to detect, and the verification of most properties (e.g., safety) is only correct for timelock-free models. Some time ago, Tripakis proposed a syntactic check on the structure of timed automata: if a certain condition (called strong non-zenoness’ SNZ) is met by all the loops in a given automaton, then zeno-timelocks are guaranteed not to occur. Checking for SNZ is efficient, and compositional (if all components in a network of automata are strongly non-zeno, then the network is free from zeno-timelocks). Strong non-zenoness, however, is sufficient-only: There exist non-zeno specifications which are not strongly non-zeno. A TCTL formula is known that represents a sufficient-and-necessary condition for non-zenoness; unfortunately, this formula requires a demanding model-checking algorithm, and not all model-checkers are able to express it. In addition, this algorithm provides only limited diagnostic information. Here we propose a number of alternative solutions. First, we show that the compositional application of SNZ can be weakened: some networks can be guaranteed to be free from Zeno-timelocks, even if not every component is strongly non-zeno. Secondly, we present new syntactic, sufficient-only conditions that complement SNZ. Finally, we describe a sufficient-and-necessary condition that only requires a simple form of reachability analysis. Furthermore, our conditions identify the cause of zeno-timelocks directly on the model, in the form of unsafe loops. We also comment on a tool that we have developed, which implements the syntactic checks on Uppaal models. The tool is also able to derive, from those unsafe loops in a given automaton (in general, an Uppaal model representing a product automaton of a given network), the reachability formulas that characterise the occurrence of zeno-timelocks. A modified version of the carrier sense multiple access with collision detection protocol is used as a case-study.     

Specifying and verifying a broadcast and a multicast snooping cachecoherence protocol

We develop a specification methodology that documents and specifies a cache coherence protocol in eight tables: the states, events, actions, and transitions of the cache and memory controllers. We then use this methodology to specify a detailed, modern three-state broadcast snooping protocol with an unordered data network and an ordered address network that allows arbitrary skew. We also present a detailed specification of a new protocol called multicast snooping (Bilir et al., 1999) and, in doing so, we better illustrate the utility of the table-based specification methodology. Finally, we demonstrate a technique for verification of the multicast snooping protocol, through the sketch of a manual proof that the specification satisfies a sequentially consistent memory model     

Integration of behavioural requirements specification within compositional knowledge engineering

In this paper it is shown how specification of behavioural requirements from informal to formal can be integrated within knowledge engineering. The integration of requirements specification has addressed, in particular: the integration of requirements acquisition and specification with ontology acquisition and specification, the relations between requirements specifications and specifications of task models and problem solving methods, and the relation of requirements specification to verification.     

A top-down methodology for microprocessor validation

A major challenge in today's functional verification is the lack of a formal specification with which to compare the RTL model. We propose a novel top-down verification approach that allows specification of a design above the RTL. From this specification, it is possible to automatically generate assertion models and RTL reference models. We also demonstrate that symbolic simulation and equivalence checking can be applied to verify an RTL design against its specification.     

基于协议形式化描述的网络增值服务开发方法与技术

增值服务是在原有网络的软硬件基础之上进行的功能开发，它在不影响原系统功能的前提下实现功能附加，使网络功能得到增值．本文引入形式化描述技术，提出了基于协议形式化描述的网络增值服务开发方法，并通过对文件传输协议的描述讨论了该方法的具体应用．最后总结了该方法在实际网络增值开发中的应用技术．     

Formal Verification of Activity-Based Specification of Protocols

In this paper, we describe a method to formally verify activity-based specifications such as EBSDL. Starting from EBSDL-like specifications that specify engineering activities in terms of input and output behaviors, we derive programs in an asynchronous language CSP-R. CSP-R programs are then verified by the Maxpar method by composing them with the programs abstracting their environment. EBSDL-like specification and its verification using our method, is illustrated through the example of a fragment of LAPD protocol. The derivation of programs from the specification of activities of the underlying protocols through EBSDL-like specifications provides an important useful tool for formal verification of real-time protocols. We shall also discuss a translation of EBSDL-like specifications to synchronous languages such as Esterel. In the method proposed, it is possible for the user to choose asynchronous or synchronous formalisms depending upon the requirements of verification vis-a-vis logical specification.     

Ptolemy离散事件模型形式化验证方法

Ptolemy是一个广泛应用于信息物理融合系统的建模和仿真工具包,主要通过仿真的方式保证所建模型的正确性.形式化方法是保证系统正确性的重要方法之一.本文提出了一种基于形式模型转换的方法来验证离散事件模型的正确性.离散事件模型根据不同事件的时间戳触发组件,时间自动机模型能够表达这个特征,因此选用Uppaal作为验证工具.首先定义了离散事件模型的形式语义,其次设计了一组从离散事件模型到时间自动机的映射规则.然后在Ptolemy环境中实现了一个插件,可以自动将离散事件模型转换为时间自动机模型,并通过调用Uppaal验证内核完成验证.最后以一个交通信号灯控制系统为例进行了成功的转换和验证,实验结果证实了该方法能够验证Ptolemy离散事件模型的正确性.     

Verification of Mondex electronic purses with KIV: from transactions to a security protocol

The Mondex case study about the specification and refinement of an electronic purse as defined in the Oxford Technical Monograph PRG-126 has recently been proposed as a challenge for formal system-supported verification. In this paper we report on two results. First, on the successful verification of the full case study using the KIV specification and verification system. We demonstrate that even though the hand-made proofs were elaborated to an enormous level of detail we still could find small errors in the underlying data refinement theory, as well as the formal proofs of the case study. Second, the original Mondex case study verifies functional correctness assuming a suitable security protocol. We extend the case study here with a refinement to a suitable security protocol that uses symmetric cryptography to achieve the necessary properties of the security-relevant messages. The definition is based on a generic framework for defining such protocols based on abstract state machines (ASMs). We prove the refinement using a forward simulation. J. C. P. Woodcock     

Integrating formal verification and conformance testing for reactive systems

In this paper, we describe a methodology integrating verification and conformance testing. A specification of a system - an extended input-output automaton, which may be infinite-state - and a set of safety properties ("nothing bad ever happens") and possibility properties ("something good may happen") are assumed. The properties are first tentatively verified on the specification using automatic techniques based on approximated state-space exploration, which are sound, but, as a price to pay for automation, are not complete for the given class of properties. Because of this incompleteness and of state-space explosion, the verification may not succeed in proving or disproving the properties. However, even if verification did not succeed, the testing phase can proceed and provide useful information about the implementation. Test cases are automatically and symbolically generated from the specification and the properties and are executed on a black-box implementation of the system. The test execution may detect violations of conformance between implementation and specification; in addition, it may detect violation/satisfaction of the properties by the implementation and by the specification. In this sense, testing completes verification. The approach is illustrated on simple examples and on a bounded retransmission protocol.     

TCBV:一种构件时序行为建模与相容性验证工具

利用形式化方法对复杂实时构件系统的时序行为进行建模与验证对于提高安全攸关实时构件系统的正确性、可靠性与安全性具有重要意义。介绍了基于时间行为协议的构件时序行为的形式化建模和相容性验证方法,给出了时间行为协议建模与相容性验证工具TCBV的系统架构与功能模块。TCBV应用方便,能够实现实时构件时序行为模型的图形化表示,并可对复杂交互行为的相容性进行自动验证。结合应用实例,介绍了如何利用TCBV对复杂实时构件系统的时序行为进行建模和验证。最后,将TCBV与其它相关工具进行了比较。     

Specification and Verification of Agent Interaction using Social Integrity Constraints

In this paper we propose a logic-based social approach to the specification and verification of agent interaction. We firstly introduce integrity constraints about social acts (called Social Integrity Constraints) as a formalism to express interaction protocols and to give a social semantics to the behavior of agents, focusing on communicative acts. Then, we discuss several possible kinds of verification of agent interaction, and we show how social integrity constraints can be used to verify some properties in this respect. We focus our attention on static verification of compliance of agent specifications to interaction protocols, and on run-time verification, based on agents' observable behavior. We adopt as a running example the NetBill security transaction protocol for the selling and delivery of information goods.