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

1999 | Buch

Integrated Formal Verification: Using Model Checking with Automated Abstraction, Invariant Generation, and Theorem Proving Kapitel lesen Erstes Kapitel lesen

Theoretical and Practical Aspects of SPIN Model Checking

5th and 6th International SPIN Workshops Trento, Italy, July 5, 1999 Toulouse, France, September 21 and 24, 1999 Proceedings

herausgegeben von: Dennis Dams, Rob Gerth, Stefan Leue, Mieke Massink

Verlag: Springer Berlin Heidelberg

Buchreihe : Lecture Notes in Computer Science

Enthalten in: Professional Book Archive

Einloggen, um Zugang zu erhalten
insite
SUCHEN

Über dieses Buch

Increasing the designer’s con dence that a piece of software or hardwareis c- pliant with its speci cation has become a key objective in the design process for software and hardware systems. Many approaches to reaching this goal have been developed, including rigorous speci cation, formal veri cation, automated validation, and testing. Finite-state model checking, as it is supported by the explicit-state model checkerSPIN,is enjoying a constantly increasingpopularity in automated property validation of concurrent, message based systems. SPIN has been in large parts implemented and is being maintained by Gerard Ho- mann, and is freely available via ftp fromnetlib.bell-labs.comor from URL http://cm.bell-labs.com/cm/cs/what/spin/Man/README.html. The beauty of nite-state model checking lies in the possibility of building \push-button" validation tools. When the state space is nite, the state-space traversal will eventually terminate with a de nite verdict on the property that is being validated. Equally helpful is the fact that in case the property is inv- idated the model checker will return a counterexample, a feature that greatly facilitates fault identi cation. On the downside, the time it takes to obtain a verdict may be very long if the state space is large and the type of properties that can be validated is restricted to a logic of rather limited expressiveness.

Inhaltsverzeichnis

Frontmatter

Part I:Selection of Papers Presented at 5thSPIN99

Keynote Address

Integrated Formal Verification: Using Model Checking with Automated Abstraction, Invariant Generation, and Theorem Proving
Abstract
Mechanized formal methods that use both model checking and theorem proving seem to hold most promise for the future. Effective use of both technologies requires they be recast as methods for calculating properties of specifications, rather than merely verifying them. The most valuable properties are those that contribute to the development of invariants and property-preserving abstractions. We outline an architecture for verification tools based on iterated use of such capabilities.
John Rushby

Theory

Runtime Efficient State Compaction in Spin
Abstract
Spin is a verification system that can detect errors automatically by exploring the reachable state space of a system. The efficiency of verifiers like Spin depends crucially on the technique used for the representation of states. A number of recent proposals for more compact representations reduce the memory requirements, but cause a considerable increase in execution time. These methods could be used as alternatives when the standard state representation exhausts the memory, but this is exactly when the additional overhead is least affordable.
We describe a simple but effective state representation scheme that can be used in conjunction with Spin’s normal modes of operation. We compare the idea to Spin’s standard state representation and describe how Spin was modified to support it. Experimental results show that the technique provides a valuable reduction in memory requirements and simultaneously reduce the execution time. For the cases considered an average reduction in memory requirements of 40% was measured and execution time was reduced on average by 19%. The proposed technique could therefore be considered to replace the default technique in Spin.
J Geldenhuys, P J A de Villiers, John Rushby
Distributed-Memory Model Checking with SPIN
Abstract
The main limiting factor of the model checker SPIN is currently the amount of available physical memory. This paper explores the possibility of exploiting a distributed-memory execution environment, such as a network of workstations interconnected by a standard LAN, to extend the size of the verification problems that can be successfully handled by SPIN. A distributed version of the algorithm used by SPIN to verify safety properties is presented, and its compatibility with the main memory and complexity reduction mechanisms of SPIN is discussed. Finally, some preliminary experimental results are presented.
Flavio Lerda, Riccardo Sisto
Partial Order Reduction in Presence of Rendez-vous Communications with Unless Constructs and Weak Fairness
Abstract
If synchronizing (rendez-vous) communications are used in the Promela models, the unless construct and the weak fairness algorithm are not compatible with the partial order reduction algorithm used in Spin’s verifier. After identifying the wrong partial order reduction pattern that causes the incompatibility, we give solutions for these two problems. To this end we propose corrections in the identification of the safe statements for partial order reduction and as an alternative, we discuss corrections of the partial order reduction algorithm.
Dragan Bošnački
Divide, Abstract, and Model-Check
Abstract
The applicability of model-checking is often restricted by the size of the considered system. To overcome this limitation, a number of techniques have been investigated. Prominent among these are data independence, abstraction, and compositionality. This paper presents a methodology based on deductive reasoning and model-checking which combines these techniques. As we show, the combination of abstraction and compositionality gives a significant added value to each of them in isolation. We substantiate the approach proving safety of a sliding window protocol of window size 16 using Spin and PVS.
Karsten Stahl, Kai Baukus, Yassine Lakhnech, Martin Stefen

Part II: Papers Presented at 6thSPIN99

Keynote Address

Formal Methods Adoption: What’s Working, What’s Not!
Abstract
Drawing from the author’s twenty years of experience in formal methods research and development, and, particularly, with the EVES-based systems, this paper provides personal impressions on what is and what is not working with regards to the adoption and application of formal methods. As both the community’s understanding of technology transfer issues and formal methods technology improve, one is optimistic that formal methods will play an increasingly important role in industry. However, significant impediments continue to exist with, perhaps, the increasing complexity of systems being both a blessing and a curse.
Dan Craigen

Methodology

Model Checking for Managers
Abstract
Model checking is traditionally applied to computer system design. It has proven to be a valuable technique. However, it requires detailed specifications of systems and requirements, and is therefore not very accessible. In this paper we show how model checking can be applied in the context of business modeling and analysis by people that are not trained in formal techniques. Spin is used as the model checker underlying a graphical modeling language, and requirements are specified using business requirements patterns, which are translated to LTL. We illustrate our approach using a business model of an insurance company.
Wil Janssen, Radu Mateescu, Sjouke Mauw, Peter Fennema, Petra van der Stappen
Xspin/Project - Integrated Validation Management for Xspin
Abstract
One of the difficulties of using model checkers “in the large” is the management of all (generated) data during the validation trajectory. It is important that the results obtained from the validation are always reproducible. Without tool support, the quality of the validation process depends on the accuracy of the persons who conduct the validation. This paper discusses Xspin/Project, an extension of Xspin, which automatically controls and manages the validation trajectory when using the model checker Spin.
Theo C. Ruys

Applications I

Analyzing Mode Confusion via Model Checking
Abstract
Mode confusion is a serious problem in aviation safety. Today’s complex avionics systems make it difficult for pilots to maintain awareness of the actual states, or modes, of the flight deck automation. NASA explores how formal methods, especially theorem proving, can be used to discover mode confusion. The present paper investigates whether state-exploration techniques, e.g., model checking, are better able to achieve this task than theorem proving and also to compare the verification tools MurØ, SMV, and Spin for the specific application. While all tools can handle the task well, their strengths are complementary.
Gerald Lüttgen, Victor Carreño
Detecting Feature Interactions in the Terrestrial Trunked Radio (TETRA) Network Using Promela and Xspin
Abstract
The problem caused by feature interactions serve to delay and increase the costs of introducing features to existing networks. We introduce a three stage technique that detects interactions in the TETRA network. Promela is used to model the network and features and its requirements are specified using linear temporal logic. The Xspin toolkit is used to verify and validate the model against its requirements.
Carl B. Adekunle, Steve Schneider
Java PathFinder A Translator from Java to Promela
Abstract
Java PathFinder [2], Jpf, is a prototype translator from Java to Promela, the modeling language of the Spin model checker [4]. Jpf is a product of a major effort by the Automated Software Engineering group at NASA Ames to make model checking technology part of the software process. Experience has shown that severe bugs can be found in final code using this technique [1], and that automated translation from a programming language to a modeling language like Promela can help reducing the effort required.
Jpf allows a programmer to annotate his Java program with assertions and verify them using the Spin model checker. In addition, deadlocks can be identied. An assertion is written as a call to an assert method dened in a predened Java class, the Verify class. The argument to the method is a boolean Java expression over the state variables. The Verify class contains additional tem- poral logic methods which allow to state temporal logic properties about static variables. Hence Java itself is used as the specication language. An application of Jpf is described elsewhere in the proceedings [3].
A respectable subset of Java is covered by Jpf, including dynamic object cre- ation, object references asrst class citizens, inheritance, exceptions, interrupts, and perhaps most importantly: thread operations. Among major concepts not translated are: packages, method overloading and overriding, method recursion, strings, and floating point numbers. Finally, the class library is not translated.
Klaus Havelund
VIP: A Visual Interface for Promela
Abstract
The Visual Interface to Promela (VIP) tool is a Java based graphical front end to the Promela specication language and the SPIN model checker [2]. VIP supports a visual formalism called v-Promela [3] which extends the Promela lan- guage with a graphical notation to describe structural and behavioral aspects of a system. v-Promela also introduces hierarchical modeling and object-oriented concepts. The formalism is largely consistent with the UML-RT proposal [5] which evolved from the Real-Time Object-Oriented Modeling (ROOM) language [4] and the Unied Modeling Language (UML) [1]. The structural part of a v- Promela model consists of structural elements called capsulesq and describes their interconnection and hierarchical nesting using a variant of UML collaboration diagrams. The behavioral aspects of a v-Promela model are described by hierar- chical communicating extended nite state machines and support such features as group transitions and optional return to history from group transitions.
The VIP tool provides a graphical v-Promela editor supporting point and click editing of v-Promela structure diagrams and hierarchically nested state machines. The editor incorporates syntax checking to warn the user about in- correct use of v-Promela graphical syntax. Storage and retrieval of models is made possible using Java serialization. The tool also has a fully integrated v- Promela compiler which generates Promela code. The resulting Promela models can be analyzed using existing SPIN technology. VIP requires the Java 1.2 Run- time Environment which is available for a variety of operating systems. VIP is not currently publicly available, but expected to be released in the near future.
Moataz Kamel, Stefan Leue

Specification and Validation

Events in Property Patterns
Abstract
A pattern-based approach to the presentation, codification and reuse of property specifications for finite-state verification was proposed by Dwyer and his colleagues in [4,3]. The patterns enable non-experts to read and write formal specifications for realistic systems and facilitate easy conversion of specifications between formalisms, such as LTL, CTL, QRE. In this paper we extend the pattern system with events — changes of values of variables in the context of LTL.
Marsha Chechik, Dimitrie O. Păun
Assume-Guarantee Model Checking of Software: A Comparative Case Study
Abstract
A variety of assume-guarantee model checking approaches have been proposed in the literature. In this paper, we describe several possible implementations of those approaches for checking properties of software components (units) using SPIN and SMV model checkers. Model checking software units requires, in general, the definition of an environment which establishes the run-time context in which the unit executes. We describe how implementations of such environments can be synthesized from specifications of assumed environment behavior written in LTL. Those environments can then be used to check properties that the software unit must guarantee which can be written in LTL or ACTL. We report on several experiments that provide evidence about the relative performance of the different assume-guarantee approaches.
Corina S. Păsăreanu, Matthew B. Dwyer, Michael Huth
A Framework for Automatic Construction of Abstract Promela Models
Abstract
One of the current trends in model checking for the verification of concurrent systems is to reduce the state space produced by the model, and one of the more promising ways to achieve this objective is to support some kind of automatic construction of more abstract models. This paper presents a proposal in this direction. The main contribution of the paper is the definition of a semantics framework which allows us to relate different models of the system, each one with a particular abstraction level. Automatic source-to-source transformation is supported by this formal basis. The method is applied to Promela models.
Maria-del-Mar Gallardo, Pedro Merino

Applications

Model Checking Operator Procedures
Abstract
Operator procedures are documents telling operators what to do in various situations. They are widely used in process industries including the nuclear power industry. The correctness of such procedures is of great importance. We describe how model checking can be used to detect potential errors and to verify properties of operator procedures. As there could be problems with modelling and model checking large systems, incremental modelling and verification is proposed as a strategy to help overcome these problems. A case study is presented to show how model checking (with the model checker Spin [5]) and the incremental strategy work in practise.
Wenhui Zhang
Applying Model Checking in Java Verification
Abstract
This paper presents our experiences in applying the Java PathFinder (Jpf), a recently developed Java to Promela translator, in the search for synchronization bugs in a Chinese Chess game server application written in Java. We give an overview of Jpf and the subset of Java that it supports and describe an initial effort to abstract and analyze the game server. Finally, we evaluate the results of the effort.
Klaus Havelund, Jens Ulrik Skakkebæk

Extensions

The Engineering of a Model Checker: the Gnu i-Protocol Case Study Revisited.
Abstract
In a recent study a series of model checkers, among which Spin [5], SMV [9], and a newer system called XMC [10], were compared on performance. The measurements used for this comparison focused on a model of the i-protocol from GNU uucp version 1.04. Eight versions of this iprotocol model were obtained by varying window size, assumptions about the transmission channel, and the presence or absence of a patch for a known livelock error. The results as published in [1] show the XMC system to outperform the other model checking systems on most of the tests. It also contains a challenge to the builders of the other model checkers to match the results. This paper answers that challenge for the Spin model checker. We show that with either default Spin verification runs, or a reasonable choice of parameter settings, the version of Spin that was used for the tests in [1] (Spin 2.9.7) can outperform the results obtained with XMC in six out of eight tests. Inspired by the comparisons, and the description in of the optimizations used in XMC, we also extended Spin with some of the same optimizations, leading to a new Spin version 3.3.0. We show that with these changes Spin can outperform XMC on all eight tests.
Gerard J. Holzmann
Embedding a Dialect of SDL in PROMELA
Abstract
We describe a translation from a dialect of SDL-88 to PROMELA, the input language of the SPIN model checker. The fairly straight- forward translation covers data types as well as processes, procedures, and services. Together with SPIN the translation provides a simulation and verification environment for most SDL features.
Heikki Tuominen
dSPIN: A Dynamic Extension of SPIN
Abstract
The SPIN extension presented in this article is meant as a way to facilitate the modeling and verification of object-oriented programs. It provides means for the formal representation of some run-time mechanisms intensively used in OO software, such as dynamic object creation and deletion, virtual function calls, etc. This article presents a number of language extensions along with their implementation in SPIN. We carried out a number of experiments and found out that an important expressibility gain can be achieved with at most a small loss of performance.
Claudio Demartini, Radu Iosif, Riccardo Sisto
Backmatter
Metadaten
Titel
Theoretical and Practical Aspects of SPIN Model Checking
herausgegeben von
Dennis Dams
Rob Gerth
Stefan Leue
Mieke Massink
Copyright-Jahr
1999
Verlag
Springer Berlin Heidelberg
Electronic ISBN
978-3-540-48234-5
Print ISBN
978-3-540-66499-4
DOI
https://doi.org/10.1007/3-540-48234-2