Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben

2000 | Buch

Formal Verification of the TTP Group Membership Algorithm Kapitel lesen Erstes Kapitel lesen

Formal Methods for Distributed System Development

FORTE / PSTV 2000 IFIP TC6 WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE XIII) and Protocol Specification, Testing and Verification (PSTV XX) October 10–13, 2000, Pisa, Italy

herausgegeben von: Tommaso Bolognesi, Diego Latella

Verlag: Springer US

Buchreihe : IFIP Advances in Information and Communication Technology

Enthalten in: Professional Book Archive

Einloggen, um Zugang zu erhalten
insite
SUCHEN

Über dieses Buch

th The 20 anniversary of the IFIP WG6. 1 Joint International Conference on Fonna! Methods for Distributed Systems and Communication Protocols (FORTE XIII / PSTV XX) was celebrated by the year 2000 edition of the Conference, which was held for the first time in Italy, at Pisa, October 10-13, 2000. In devising the subtitle for this special edition --'Fonna! Methods­ Implementation Under Test' --we wanted to convey two main concepts that, in our opinion, are reflected in the contents of this book. First, the early, pioneering phases in the development of Formal Methods (FM's), with their conflicts between evangelistic and agnostic attitudes, with their over­ optimistic applications to toy examples and over-skeptical views about scalability to industrial cases, with their misconceptions and myths . . . , all this is essentially over. Many FM's have successfully reached their maturity, having been 'implemented' into concrete development practice: a number of papers in this book report about successful experiences in specifYing and verifYing real distributed systems and protocols. Second, one of the several myths about FM's - the fact that their adoption would eventually eliminate the need for testing - is still quite far from becoming a reality, and, again, this book indicates that testing theory and applications are still remarkably healthy. A total of 63 papers have been submitted to FORTEIPSTV 2000, out of which the Programme Committee has selected 22 for presentation at the Conference and inclusion in the Proceedings.

Inhaltsverzeichnis

Frontmatter

Verification and Theorem Proving

Frontmatter
1. Formal Verification of the TTP Group Membership Algorithm
Abstract
This paper describes the formal verification of a fault-tolerant group membership algorithm that constitutes one of the central services of the Time-Triggered Protocol (TTP). The group membership algorithm is formally specified and verified using a diagrammatic representation of the algorithm. We describe the stepwise development of the diagram and outline the main part of the correctness proof. The verification has been mechanically checked with the PVS theorem prover.
Holger Pfeifer
2. Verification of a Sliding Window Protocol Using IOA and MONA
Abstract
We show how to use a decision procedure for WS1S (the MONA tool) to give automated correctness proofs of a sliding window protocol under assumptions of unbounded window sizes, buffer sizes, and channel capacities. We also verify a version of the protocol where the window size is fixed. Since our mechanized target logic is WS1S, not the finite structures of traditional model checking, our method employs only two easy reductions outside the decidable framework. Additionally, we formulate invariants that describe the reachable global states, but the bulk of the detailed reasoning is left to the decision procedure. Because the notation of WS1S is too low-level to describe complicated protocols at a reasonable level of abstraction, we use a higher level language for the protocol description, and then build a tool that automatically translates this language to the MONA syntax. The higher level language we use is IOA.
Mark A. Smith, Nils Klarlund
3. A Priori Verification of Reactive Systems
On Simultaneous Syntactic Action Refinement for TCSP and the Modal Mu-Calculus
Abstract
In this paper we present a refinement operator ·[a ↝ Q], defined both on TCSP-like process terms P and formulas cp of the Modal Mu-Calculus. We show that
the system induced by a term P satisfies a specification φ if and only if the system induced by the refined term P[α ↝ Q] satisfies the refined specification φ[α ↝ Q]
where Q is a process term from an appropriate sublanguage of TCSP. We explain how this result can be used to reason about reactive systems. In particular it supplies a method to verify systems a priori: Provided P ╞ φ holds, the refinement of φ into φ[a ↝ Q] induces a transformation of P into P[a ↝ Q] such that P[a ↝ Q] ╞ φ[a ↝ Q]. The above result holds under the restriction that the set of actions that occur in the term Q has to be disjoint from the set of actions occurring in the term P and the formula φ. Though such restrictions on alphabet disjointness are commonly adopted in approaches to syntactic action refinement for process term languages they preclude the possibility to carry out certain refinement steps that might be necessary in the stepwise development of reactive systems. We show, that while dropping the above restriction, the validity of the two implications comprised in the above result can still be established independently for different interesting fragments of the Modal Mu-Calculus.
Mila Majster-Cederbaum, Frank Salger, Maria Sorea

Test Generation

Frontmatter
4. From Rule-Based to Automata-Based Testing
Abstract
Rule based languages have been used extensively to provide a declarative description of causal relationships between events and conditions in a wide variety of systems. On the other hand, automata (finite state machine) based models provide a detailed operational specification of how the system state evolves over time. While rules are a convenient declarative mechanism, a finite automaton is more flexible and far more easily analyzed than a collection of rules with potentially complicated semantics.
In this paper, we address this dichotomy in the context of large scale testing. We describe a (probabilistic) rule based system, which has been developed and used over many years as the testing model of a large telephone switch. One important drawback of the rule-based system is that it is inflexible in terms of the test generation mechanisms it supports, essentially only allowing the generation of random tests.
We have designed and implemented a translation from the rule-based language to a probabilistic finite automaton model, and applied it to the switch model. Our translation makes use of several automata-theoretic algorithms to keep the size of the resulting automata manageable.
The automaton model allows much more flexible and targeted test generation. We have designed and implemented an assortment of targeted test generation algorithms which are applied to the probabilistic automaton.
Kousha Etessami, Mihalis Yannakakis
5. Integrated System Interoperability Testing with Applications to VoIP
Abstract
This work has been motivated by the need to test interoperability of systems carrying voice calls over the IP network. Voice over IP (VoIP) systems must be integrated and interoperate with the existing Public Switched Telephone Network (PSTN) before they will be widely adopted. Standards have been developed to address this problem, but unfortunately different standards bodies and commercial consortiums have defined different standards. Furthermore, the prevailing commercial standard (H.323) is incomplete, complex, and presents the implementers with “vendors latitudes”. As a result, there is no guarantee that the integrated VoIP systems would interoperate properly even if the implementations are all H.323-compliant. Interoperability testing has become indispensable.
We discuss criteria that cover all the required patterns of “inter-operating behavior.” We want to test all such system interoperations. On the other hand, test execution in real environment is expensive, and we want to minimize the number of tests while maintaining the coverage.
We present a general method for automatic generation of test cases, which cover all the required system interoperations and contain a minimal number of tests. We study data structures and efficient test generation algorithms, which take time proportional to the total test case size. We report experimental results on VoIP systems.
Nancy Griffeth, Ruibing Hao, David Lee, Rakesh K. Sinha
6. On Test Derivation from Partial Specifications
Abstract
The paper addresses the problem of test derivation from partially defined specifications. A specification is modeled by an Input/Output FSM such that transitions from some states on some inputs are not specified (a partial FSM). Tests have to be derived for a weak conformance relation between FSMs as a conformance relation. The paper further elaborates the state-counting approach by providing an insight into the structure of tests with fault coverage for partial deterministic machines and by offering risk-free optimizations which reduce the length of resulting tests. Based on this approach, a method for deriving tests with fault coverage guarantee (checking experiments) is proposed. It is demonstrated that the method is superior to other test derivation methods for deterministic state machines.
Alex Petrenko, Nina Yevtushenko

Model Checking — Theory

Frontmatter
7. Compositionality for Improving Model Checking
Abstract
Model checking is an automatic technique for verifying finite state systems: in this approach, properties are expressed in a temporal logic and systems are modelled as transition systems. A main problem of model checking is state explosion: very complex systems are often represented by transition systems with a prohibitive number of states. The primary cause of this problem is the parallel composition of interacting processes. Many techniques have been proposed to attack this problem, among them compositional techniques. These techniques reduce state explosion exploiting the natural decomposition of complex systems into processes. In this paper we present a formula-based compositional rule that allows us to deduce a property of a parallel composition of processes by checking it only on a component process.
Antonella Santone
8. A Model Checking Method for Partially Symmetric Systems
Abstract
A new method of model checking is proposed based on the existence of symmetries in system. We show how to fully handle the partial symmetries of both properties and systems. Our method does not depend on a particular formalism and a priori can be applied to any one. Well-formed Petri Nets are used as an illustration.
Serge Haddad, Jean-Michel Ilié, Khalil Ajami

Model Checking — Applications

Frontmatter
9. Specification and Verification of Message Sequence Charts
Abstract
The use of message sequence charts (MSCs) is popular in designing and documenting communication protocols. A recent surge of interest in MSCs has led to various algorithms for their automatic analysis, e.g., finding race conditions. In this paper we adopt a causality based temporal logic to specify properties of MSCs. This alleviates some problems that arise when specifying properties of MSCs using the traditional interleaving-based linear temporal logic: systems of MSCs are not necessarily finite state systems, leading to undecidability of LTL model checking. Even when dealing with finite state MSC systems, the set of linearizations can easily generate an exponential state space explosion. We provide an efficient model checking algorithm for systems of MSCs. Our construction models the FIFO MSC systems using a restricted version of w-automata with two successor relations. We implemented a model checking environment for MSCs as an extension to the SPIN model checking system.
Doron Peled
10. A State-Exploration Technique for Spi-Calculus Testing-Equivalence Verification
Abstract
Several verification techniques based on theorem proving have been developed for the verification of security properties of cryptographic protocols specified by means of the spi calculus. However, to be used successfully, such powerful techniques require skilled users. Here we introduce a different technique which can overcome this drawback by allowing users to carry out the verification task in a completely automatic way. It is based on the definition of an extended labeled transition system, where transitions are labeled by means of the new knowledge acquired by the external environment as the result of the related events. By means of bounding the replication of parallel processes to a finite number, and by using an abstract representation of all explicitly allowed values in interactions between the spi process and the environment, the number of states and transitions remains finite and tractable, thus enabling the use of state-space exploration techniques for performing verification automatically.
Luca Durante, Riccardo Sisto, Adriano Valenzano
11. Verification of Consistency Protocols Via Infinite-State Symbolic Model Checking
A Case Study: the IEEE Futurebus+ Protocol
Abstract
We apply infinite-state model checking to verify safety properties of a parameterized formulation of the IEEE Futurebus+ coherence protocol modeled at the behavior level in a system with split transaction. This case-study shows that verification techniques previously applied to hybrid and real-time systems can be used as tools for validating parameterized protocols. This technology transfer is achieved by combining abstraction techniques, symbolic representation via constraints, efficient operations based on real arithmetics, and reachability algorithms. To our knowledge this is the first time that safety properties for a parameterized version of the Futurebus+ protocol has been automatically verified.
Giorgio Delzanno

Multicast Protocol Analysis and Simulation

Frontmatter
12. Systematic Performance Evaluation of Multipoint Protocols
Abstract
The advent of multipoint (multicast-based) applications and the growth and complexity of the Internet has complicated network protocol design and evaluation. In this paper, we present a method for automatic synthesis of worst and best case scenarios for multipoint protocol performance evaluation. Our method uses a fault-oriented test generation (FOTG) algorithm for searching the protocol and system state space to synthesize these scenarios. The algorithm is based on a global finite state machine (FSM) model. We extend the algorithm with timing semantics to handle end-to-end delays and address performance criteria. We introduce the notion of a virtual LAN to represent delays of the underlying multicast distribution tree.
As a case study, we use our method to evaluate variants of the timer suppression mechanism, used in various multipoint protocols, with respect to two performance criteria: overhead of response messages and response time. Simulation results for reliable multicast protocols show that our method provides a scalable way for synthesizing worst-case scenarios automatically. We expect our method to serve as a model for applying systematic scenario generation to other multipoint protocols.
Ahmed Helmy, Sandeep Gupta, Deborah Estrin, A. Cerpa, Y. Yu
13. Simulating Multicast Transport Protocols in Estelle
A re-usable IP network module
Abstract
State of the art multicast research points to a future architecture in which multicast transport protocols provide end-to-end control over the IP multicast datagram service, similar to TCP/IP. However, many aspects of these protocols are still to be resolved, and are active areas of research. We present a simulation architecture for applying the Formal Description Technique Estelle to the development of multicast transport protocols. A key component of this architecture is the IP network (IPN) module, which is the focus of this paper. The IPN module reproduces complex medium behaviours specific to multicast transport protocols and not provided by existing IP medium models, including: IGMP services, network heterogeneity, address-based routing, and multicast delivery. The sophistication of the IPN module presents a realistic simulation environment for the formal investigation of multicast transport protocols. The module has in addition been designed to be independent of the upper-layer protocol being investigated, and as such presents a re-usable component for the simulation of any IP-based protocols.
Justin Templemore-Finlayson, Eugen Borcoci
14. Generation of Realistic Signalling Traffic in an ISDN Load Test System Using SDL User Models
Abstract
This paper describes the use of SDL for defining User Models for a test and measurement system whose purpose is to perform load tests of the control unit of an ISDN-PBX with realistic signalling traffic. The generation of realistic signalling traffic is based on the emulation of real users by User Models. The functional behaviour of a User Model is defined by an SDL process using a subset of the SDL syntax. The use of this type of User Models allows, besides the creation of messages according to distribution functions, to process messages received from the system under test and therefore to react appropriately on them, like a real user would do it. Normally several User Models are used together for a load test, so that the generated traffic is a realistic mixture of a variety of different user categories. The User Models are transformed to data structures for execution by the load test system. These data structures are optimized for efficiency in order to reach the target call rate of at least 30000 calls per hour on a standard workstation. The temporal behaviour of the User Models is defined separately by means of Event Generators which send signals to the User Models according to statistical distribution functions.
Thomas Steinert, Georg Rößler

Exhaustive and Probabilistic Testing

Frontmatter
15. Satisfaction Up to Liveness
Verification based on Exhaustive Testing
Abstract
An approximation to the usual linear satisfaction of temporal properties is discussed in this paper. It is called satisfaction up to liveness as it only differs from the linear satisfaction relation on liveness but not on safety properties. From the point of view of observation, satisfaction up to liveness and linear satisfaction are indistinguishable. Roughly speaking, by observing all finite behaviours (exhaustive testing), we do not know whether a system satisfies a property up to liveness or linearly. Being indistinguishable from linear satisfaction in terms of complete observations, satisfaction up to liveness offers an alternative approach to model-checking.
Ulrich Ultes-Nitsche
16. Testing IP Routing Protocols — From Probabilistic Algorithms to a Software Tool
Abstract
We present probabilistic algorithms for testing IP routing protocols. Different than commercial testing tools, which select their test cases in an ad-hoc manner, our technique chooses test cases with a guaranteed fault coverage. Our algorithms are applied to testing RIP, OSPF, and BGP routing protocols. We test the routing table correctness, database information consistency with network topology and packet forwarding behaviors. We provide an analysis of test execution time and fault coverage. The algorithms are part of a software tool SOCRATES, developed at Bell laboratories. SOCRATES also creates a testing environment so that the generated test cases can be executed in real time on high speed routers.
Ruibing Hao, David Lee, Rakesh K. Sinha, Dario Vlah

Hardware Specification, Implementation and Testing

Frontmatter
17. Verifying and Testing Asynchronous Circuits Using Lotos
Abstract
It is shown how Dill (Digital Logic in Lotos) can be used to specify, verify and test asynchronous (unclocked) hardware designs. New relations for (strong) conformance are defined for assessing a circuit implementation against its specification. An algorithm is also presented for generating and applying implementation tests based on a specification. Tools have been developed for automated verification of conformance and generation of tests. The approach is illustrated with three case studies that explore speed independence, delay insensitivity and testing of sample asynchronous circuits.
Ji He, Kenneth J. Turner
18. Hardware Implementation of Concurrent Periodic EFSMs
Abstract
This paper proposes a concurrent periodic EFSMs model and a technique to synthesize hardware circuits from real-time system specifications in this model. In the proposed model, the data exchange by synchronous execution of the same events in multiple EFSMs (multi-way synchronization) can be specified like LOTOS. The executable time range of each event can be specified as a logical conjunction of linear inequalities of the execution time of its preceding events, constants and integer variables with some values input from environments. Here, we assume that every event sequence starting from the initial state in each EFSM returns to the initial state in the specified time interval. The proposed synthesis technique implements only executable combination of branches in a given specification with a schedule table which guarantees that if each I/O event is executed within the specified time range, at least one of the following event sequences remains executable. Some experiments show that the performance and size of the generated circuits are reasonable for practical use.
Hisaaki Katagiri, Masayuki Kirimura, Keiichi Yasumoto, Teruo Higashino, Kenichi Taniguchi
19. Modeling Distributed Embedded Systems In Multiclock Esterel
Abstract
In this paper, we show that the paradigm of Multiclock Esterel can be effectively used for the design of asynchronously communicating distributed systems. First we show that the protocol used in Multiclock Esterel for the modeling of VHDL can be used for the design of asynchronous interaction of processes, and an analysis can be made relative to speed or periodicity of the underlying processes for a safe implementation without missing any signals. The analysis also shows that one can arrive at a tradeoff between the periodicity and the buffer requirements on the average over a sequence of periods. Then, we illustrate the modeling of communicating reactive processes (which is essentially a network of Esterel nodes communicating via the rendezvous mechanism) as an instance of Multiclock Esterel.
Basant Rajan, R. K. Shyamasundar

Formal Semantics

Frontmatter
20. Compact Net Semantics for Process Algebras
Abstract
Process algebras and Petri nets are two well known formal methods. In the literature, several mappings from process algebras to Petri nets have been proposed to provide a truly concurrent semantic framework to concurrent programming languages. From an applicative point of view, such mappings facilitate the integration and the cross fertilization between the two formalisms, making it possible the development of a multiparadigm methodology for the modeling and analysis of concurrent systems since the early stages of their design. In this paper we define a new Petri net semantics for process algebras, we demonstrate that it improves the previous proposals with respect to the size of the resulting nets, and we illustrate the usefulness of the net semantics by showing how to reinterpret at the process algebra level results efficiently obtainable at the Petri net level.
Marco Bernardo, Marina Ribaudo, Nadia Busi
21. A Concise Compositional Statecharts Semantics Definition
Abstract
Statecharts is a well-known specification language for modeling system behavior. Its intuitive graphical appeal for specifying hierarchical, concurrent state machines conceals the difficulties in formalizing its semantics. The causes are in Statecharts’ two-level semantics when demanding compositionality, as is necessary in order to obtain easy comprehensibility and modularity of system specifications. This paper suggests a compositional approach for formalizing the Statecharts semantics directly on sequences of micro steps using labeled transition systems as semantical domain. Though we consider causality, global consistency, as well as the synchrony hypothesis, our approach results in a very short and concise semantics definition of Statecharts.
Michael von der Beeck
22. Implementing CCS in Maude
Abstract
We explore the features of rewriting logic and the language Maude as a logical and semantic framework for representing both the semantics of CCS, and a modal logic for describing local capabilities of CCS processes. Although a rewriting logic representation of the CCS semantics was given previously, it cannot be directly executed in the default interpreter of Maude. Moreover, it cannot be used to answer questions such as which are the successors of a process after performing an action, which is used to define the semantics of the modal logic. Basically, the problems are the existence of new variables in the righthand side of the rewrite rules and the nondeterministic application of the semantic rules, inherent to CCS. We show how these problems can be solved by exploiting the reflective properties of rewriting logic, which allow controlling the rewriting process. This executable specification plus the reflective control of the rewriting process can be used to analyze CCS processes.
Alberto Verdejo, Narciso Martí-Oliet

Invited Papers on Verification and Security

Frontmatter
23. From Refutation to Verification
Abstract
Model checking has won some industrial acceptance in debugging designs. Theorem proving and formal verification are less popular. An approach built around automated abstractions could integrate theorem proving with model checking in an acceptable way and provide a bridge between refutation and verification.
John Rushby
24. Process Algebraic Analysis of Cryptographic Protocols
Abstract
Recent approaches to the analysis of crypto-protocols build on concepts which are well-established in the field of process algebras, such as labelled transition systems (Its) and observational semantics. We outline some recent work in this direction that stems from using cryptographic versions of the pi-calculus ¡ª most notably Abadi and Gordon’s spi-calculus — as protocol description languages. We show the impact of these approaches on a specific example, a simplified version of the Kerberos protocol.
Michele Boreale, Rocco De Nicola, Rosario Pugliese
25. A Logic of Belief and a Model Checking Algorithm for Security Protocols
Abstract
Model checking is a very successful technique which has been applied in the design and verification of finite state concurrent reactive processes. In this paper we show how this technique can be used for the verification of security protocols using a logic of belief. The underlying idea is to treat separately the temporal evolution and the belief aspects of principals. In practice, things work as follows: when we consider the temporal evolution of a principal we treat belief atoms (namely, atomic formulae expressing belief) as atomic propositions. When we deal with the beliefs of a principal A, we model its beliefs about another principal B as the fact that A has access to a representation of B as a process. Then, any time it needs to verify the truth value of some belief atom about B, e.g., B B ø, A simply tests whether, e.g., ø holds in its (appropriate) representation of B. Beliefs are essentially used to control the “jumping” among processes. Our approach allows us to reuse the technology and tools developed in model checking.
M. Benerecetti, F. Giunchiglia, M. Panti, L. Spalazzi
Metadaten
Titel
Formal Methods for Distributed System Development
herausgegeben von
Tommaso Bolognesi
Diego Latella
Copyright-Jahr
2000
Verlag
Springer US
Electronic ISBN
978-0-387-35533-7
Print ISBN
978-1-4757-5264-9
DOI
https://doi.org/10.1007/978-0-387-35533-7