Abstracts from SPIN95, the First SPIN Workshop

Held at INRS-Télécommunications, Montréal, Quebec

On 16 October 1995

• Table of Contents from the SPIN95 Workshop Proceedings

Index of Papers Presented at the Workshop:

1. Verifying Semantic Relations in SPIN
2. Checking Linear Temporal Logic Properties
3. Partial Order Reduction of the State Space
4. The ULG Partial Order Package for SPIN
5. Issues in State Space Reduction
6. Security Protocol Verification using SPIN
7. Implementing MSCs in PROMELA
8. Reactive SPIN and PROMELA
9. Industrial experience with formal validation
10. Process Control Design Using SPIN
11. Modeling and Verification of the RUBIS micro-kernel with SPIN
12. Design of a Storm Surge Barrier control System
13. Two applications of PROMELA/SPIN
14. SPIN as a Hardware Design Tool

Index of Complementary Material:

1. Interactive Timed Simulation of Distributed Systems
2. Extending PROMELA and SPIN for Real-Time
3. Specification and Verification of the Implementation Behavior of a Wireless LAN Controller Chip using PROMELA and SPIN
4. Using OBDD Encodings for Space Efficient State Storage during On-the-fly Model Checking

Participation

Printed Proceedings

SPIN96?

Abstracts:

Hakan Erdogmus, National Research Council, Canada

• Postscript of full paper
• SPINe is an experimental verification system based on PROMELA/SPIN version 1.5.7. The SPINe system extends SPIN with limited semantics relation checking capabilities implemented in terms of a new option -e, whose usage is given below.

  	spine -eRel fileL fileR
  

  Here Rel indicates the particular semantic relation (usually a preorder or an equivalence) to be verified (trace inclusion, trace equivalence, testing equivalence), and fileL and fileR are two files containing the PROMELA models to be compared.

Doron Peled and Gerard Holzmann, AT&T Bell Laboratories, NJ, USA

• Postscript of full paper
• A new version of SPIN is described, in which standard linear temporal logic (LTL) notation, as developed by Manna and Pnueli, can be used for expressing properties of PROMELA models. This allows asserting properties of concurrent programs using the LTL operators such as <> (eventually), [] (always) and U (until), combined using the usual Boolean operations (and, or, not, implies). For example, the property []<> p -> <> q (always eventually p implies eventually q) means that if p happens always eventually, or in other words, infinitely often, then q will eventually happen.

  An efficient algorithm translates LTL formulae directly into PROMELA's never claims, allowing immediate automatic verification by SPIN. Although in general the translation gives an exponential automaton, the algorithm performs quite well on the temporal formulas typically encountered in verification.

Doron Peled and Gerard Holzmann, AT&T Bell Laboratories, NJ, USA

• Postscript of full paper
• Partial order reduction for model-checking is an approach to reduce the state space explosion caused when verifying concurrent programs and protocols. It is based on the observation that in many cases the relative order of concurrent actions of a program is unimportant to the checked property. By fixing some arbitrary order, and avoiding all possible orders, a significant gain in memory and time can be achieved in many cases. Sequences that are equivalent up to the order of concurrent actions are grouped together, and the reduction algorithm guarantees to generate a state space which contains at least one sequence per equivalence class.

  We describe the new version of SPIN which incorporates a partial order reduction technique. Experimental results show significant reductions. The partial order reduction affects how a subset of the successors are selected from each state, to guarantee that at least one sequence per equivalence class is generated. Care is taken to minimize the time and space used to calculate these subsets. Thus, achieving the reduction with least overhead. The reduction algorithm preserves safety and liveness properties of LTL. Parts of the reduction algorithm have been formally verified using the theorem prover HOL.

Patrice Godefroid, AT&T Bell Laboratories, IH, USA

• Postscript of full paper
• This document presents an overview of the partial order package for SPIN developed at the University of Liege (ULg) in 1992-1994. The current version of the ULg Partial Order Package is available free of charge for educational and research purposes by anonymous ftp from ftp.montefiore.ulg.ac.be in the /pub/popackage directory.

Jean-Charles Grégoire, INRS-Télécom, Canada

• Postscript of full paper
• The paper describes some of the results of experiments performed at INRS-Télécommunications on various extensions of SPIN. Our goal is to expose some possible avenues of evolution of the PROMELA language and its tool. My vision of PROMELA is of a language with two distinct components. A reactive component has the nondeterministic constructs (if,do), the processes as well as the communications. A deterministic component is responsible for the computations.

Audun Joesang, Norwegian Inst. of Technology, Norway

• Postscript of full paper
• This paper presents some ideas on how SPIN/PROMELA can be adapted to cover security protocol verification. Existing methods are usually based on logical deduction, and we briefly describe the strength and weaknesses of BAN logic which is the method most widely used. The goal of using SPIN for this purpose is to have a new approach to security protocol verification, and to find a method which is strong where other methods are weak. A brief description of a practical realisation is given, and the difficulties which are pointed out is the specification and implementation of the model, and the state space explosion.

Stefan Leue, University of Waterloo, Canada

• Postscript of full paper
• We have previously defined a formal semantics for Message Flow Graphs and Message Sequence Charts, capturing most of the syntactic features contained in the ITU-T recommendation Z.120. We discuss here a translation of MSCs into PROMELA, and report on experiments executing the PROMELA code using the SPIN simulator and validator.

Elie Najm and Fred Olsen, ENST, France

• Postscript of full paper
• Reactive PROMELA is an extension to the PROMELA language which lets the user specify configurations of reactive automata. This provides a simple and powerful way to decompose a system. To simulate and verify systems written in Reactive PROMELA the tool Reactive SPIN has been developed. It is a preprocessor for SPIN which translates a Reactive PROMELA system into a corresponding PROMELA system. The translated system can then be simulated and verified using SPIN. The main function performed by Reactive SPIN is to combine configurations of automata into PROMELA proctypes. We demonstrate the language and the tool with the specification and verification of the HDLC protocol.

Mark Staskauskas, AT&T Bell Labs, IH, USA

• Postscript of full paper
• We have developed a formal validation tool that has been used in several projects that are developing software for AT&T's 5ESS(tm) telephone switching system. The tool validates networks of communicating processes specified in virtual finite state machine (vfsm) notation, which is used during the low-level design phase of software development to specify the control behavior of an implementation. The vfsm validator performs a reachability analysis, using Holzmann's bitstate-hashing technique, to check for errors in vfsm communication such as deadlock, livelock and unexpected inputs. In this paper we present an overview of the vfsm methodology and validator, report in the present status of the vfsm validation effort, and discuss some of the lessons we have learned about the proper role of formal validation in the software development process.

Thierry Cattel, EPFL, Switzerland

• Postscript of full paper
• This paper reports an experience with the modeling, verification and concurrent implementation of a medium-size process control problem. The case study was proposed by Forschungszentrum Informatik, Karslruhe in 1993 in order to promote the usage of formal methods in industry. It concerns an industrial robotics application that processes metal plates. A top-down design approach is followed where successive CCS and PROMELA specification levels of decreasing abstraction are considered, each layer little by little allows verification of parts of the security requirements this providing a mean for coping with state explosion. The level refinements are checked with the Concurrency Workbench, a CCS-based tool. Safety and liveness requirements are checked in linear temporal logic and checked with SPIN.

  From the ultimate specification two different implementations are derived. The first one is in Synchronous C++, a concurrent extension of C++, and the second is in Regis/Darwin. This application shows that SPIN is quite appropriate for developing control process problem from scratch and with requirements to be checked in mind. It appeared clearly that the specification phase was very important for obtaining a satisfactory specification from which a well behaved implementation was derived easily in a few days.

Greg Duval and Jacques Julliand, EPFL, Switzerland

• Postscript of full paper
• This experience was lead at the Laboratoire Informatique de Besancon and its aim was the modeling and verification of the RUBIS kernel, a multitaskin multiprocessor operating system. Another aim of this study was to find out a method to formalize and to verify such systems. The first results are given. A modeling approach is used and we formalize the models of the system, the scenarios and the properties in PROMELA and linear temporal logic. Two kinds of models are produced, the so-called abstract models and detailed models which are model-checked with the SPIN tool. An exhaustive verification of the intertask communication features of RUBIS was carried out. It revealed several problems in the management of error return codes. This paper gives hints of a method to construct and formalize the models of an operating system such as RUBIS.

Pim Kars, Univ. Twente, The Netherland

• Postscript of full paper
• The SPIN tool ste (SPIN and XSPIN) was used to validate parts of the design of a storm surge barrier control system, in particular the communication interfaces with the outside world. PROMELA combined with Z is used to specify crucial aspects of the design. In this talk we outline our experience with the use of SPIN and PROMELA, and discuss some ideas for extensions and improvements.

F. Joe Lin, Bellcore, NJ, USA

• Postscript of full paper
• Errors such as deadlock and race conditions are common yet difficult to debug in client/server models based on remote procedure call and multi-threading. This paper presents an effective approach to detect these errors. It shows how to apply the specification and validation techniques in protocol engineering to discover those errors in the early stages of a development. The work is based on the protocol specification and validation tool PROMELA/SPIN. PROMELA is extended to a new language called PROMELA-C/S for additional expressive power of specifying client/server communications. A PROMELA-C/S translator then is built to convert PROMELA-C/S to PROMELA for running validations using SPIN.

Budi Rahardjo, U. of Manitoba, Canada

• Postscript of full paper
• This paper presents the application of SPIN to verify a hardware design. A hazardous circuit is modeled in PROMELA and verified with SPIN. SPIN show the presence of the hazard. The circuit was corrected and verified.

Other Papers

Marco Daniele, Paola Renditore, and Roberto Manione, CSELT, Italy

• Postscript of full paper
• The present paper presents an approach to timed interactive simulation based on the execution of timed CSP-like models; the language presented is PROMELA+, derived from PROMELA with the extension to temporal quantification. The simulation environment, named YES, includes also a statistical analyzer which requests to the executor as many samples as needed to generate the desired estimators with the given properties.

Stavros Tripakis and Costas Courcoubetis, Crete

• Postscript of full paper
• The efficient representation and manipulation of time information is key to any successful implementation of a verification tool. Two slightly different models of timed automata have been proposed in the literature. We extend the syntax and semantics of the higher level specification language PROMELA to include constructs and statements based on the above models. We implemented this extension on top of the verification tool SPIN.

Michael Griffioen, AT&T Network Wireless Systems, The Netherlands

• For full paper, contact: Michael.Griffioen@utrecht.attgis.com
• This paper describes an industrial application of SPIN and PROMELA at AT&T Network Wireless Systems in Utrecht, The Netherlands. SPIN/PROMELA are used for the specification and verification of distributed behavior in an implementation of a Wireless Medium Access Control Protocol using a combined hardware and software implementation architecture. The correctness of the implementation level design is regarded as very important. SPIN/PROMELA are used to specify and verify designs at three different levels:
  1. the design of individual (distributed) algorithms,
  2. the design of the composite, implementation independent, functionality, and
  3. the design on the implementation level.
  Although at the outset SPIN and PROMELA appeared largely suitable for these purposes, several problems were anticipated in the practical application in an industrial environment. These problems were identified and solutions were implemented in SPIN. The result is that SPIN/PROMELA is now suited for specification and verification of designs at abstract as well as implementation levels of detail. This paper gives a survey of specific problems concerning PROMELA semantics and SPIN verification capabilities, and how they were solved.

Willem C. Visser, Manchester Univ., UK

• For full paper, contact: visserw@cs.man.ac.uk
• The use of an Ordered Binary Decision Diagram (OBDD) to store all visited states during on-the-fly model checking (or reachability analysis) is investigated. To improve the time and space efficiency a novel state compression technique is introduced. This compression technique is safe, in the sense that no two unique states will have the same compressed representation. A number of real-world (as opposed to contrived) examples are used to evaluate an experimental implementation of the OBDD state store within the SPIN validation tool. In all the examples a reduction in space is achieved when using the OBDD state store as opposed to the more traditional hash table state store. The memory and time usage when combining partial orders with the OBDD state store is also considered.

Return to