Abstract Starting with the observation that many verification problems can be reduced to deciding various forms of state reachability, this talk then examines how the latter can be done in the context of infinite state systems. It identifies the central problem to be solved as computing, in a way that can generate an infinite number of states in a finite amount of time, the fixpoint of the (forwards or backwards) transition relation of the program to be analyzed. Doing this requires three basic components: a finite representation for infinite sets of states together with the algorithms for manipulating it; a technique for bootstrapping from finite to infinite sets of states; and a termination criterion. For the first component, its is shown that regular sets play a central role. For the second, a variety of techniques are discussed, but one, the "loop-first search", is emphasized. For the third, it is argued that termination detection is sufficient and that termination guarantee offers little additional practical advantage beyond a theoretical illusory peace of mind.
Abstract
The verification algorithm of SPIN is based on an
explicit enumeration of a subset of the reachable
state-space of a system that is obtained through
the formalization of a correctness requirement
as an $omega#-automaton.
This $omega#-automaton restricts the state-space
to precisely the subset that may contain the counter-examples
to the original correctness requirement, if they exist.
This method of verification conforms to the method
for automata-theoretic verification outlined in [VW86].
SPIN derives much of its power from an efficient implementation
of the explicit state enumeration method in this context.
The maximum number of reachable states that can
be stored in main memory with this method, either explicitly
or implicitly, then determines the maximum problem size
that can be solved.
We review some methods that have been tried to
reduce the amount memory used per state,
and describe some new
methods that achieve relatively high compression rates.
Abstract Partial order reduction methods form a collection of state exploration techniques set to relieve the state explosion problem in concurrent program verification. One such method is implemented in the verification tool SPIN. Its use often reduces significantly the memory and time needed for verifying local and termination properties of concurrent programs, and, moreover, for verifying that concurrent programs satisfy their linear temporal logic specifications (i.e., for LTL model-checking). This paper builds on SPIN's partial order reduction method to yield an approach which enables further reductions in space and time for verifying concurrent programs.
Abstract PROMELA is a language for modeling concurrent systems, developed specifically for describing communication protocols. Analysis of some properties of PROMELA models is automated by the SPIN model checker. Currently, the semantics of PROMELA is most completely and accurately defined by the C implementation of SPIN. It would be preferable to have a formal definition of PROMELA semantics independent of this implementation. This report describes an operational semantic definition for most of PROMELA in the logic of ACL2 [KM94]. It should be considered a preliminary version which can be refined in response to public scrutiny.
Abstract An approach to a formal semantics definition for PROMELA is presented. The approach uses SOS rules to define a labeled transition system model for a PROMELA program. The approach is a bottom-up, incremental approach with three basic steps (declarations, single processes, parallel processes). PROMELA before version 2.0 is treated nearly entirely. Especially assertions, never claims, and correctness conditions are discussed.
Abstract SPIN is a tool for the simulation and verification of protocols. PROMELA its source language, is a formal description technque like SDL and Estelle that is based on communicating state machines. The tool and the language are in the public domain and therefore widely used. The "Steam-Boiler Control Specification Problem" consists of an informal specification of a steam boiler system in a nuclear power plant. In this paper we show that PROMELA is suitable for the description of a technical system like the steam boiler. We describe the methods which we used to translate the informal problem description into a PROMELA specification. Further, we present our extensions to the SPIN system, which allow an automatic generation of compiled implementations from PROMELA sourcecode. We summarize the extensions to PROMELA that we found necessary for the creation of the implementation.
Abstract Harel proposed the graphical language statecharts[Harel87] for specifying behavior of reactive systems. Statecharts extend Mealy machines by parallelism and hierarchy. The communication mechanism in statecharts is instantaneous broadcase and the concurrency model is maximal parallelism. Our research concerns a compiler from statecharts to PROMELA/SPIN in order to exploit state space reduction techniques implemented in SPIN (e.g., partial order reduction) for statecharts.
Abstract This paper demonstrates robustness and effectiveness of a Group Address Registration Protocol (GARP) by succesful use of SPIN. GARP is a datalink-level protocol for dynamically joining and leaving multicast groups on a bridged LAN. It is currently in the process of standardization as part of IEEE P802.lp. SPIN is used to verify a model of multicast-base LAN described in PROMELA. The protocol has been proved to be free from incorrectness such as unspecified receptions and deadlocks. It has also been proved that there is no violation of a temporal claim for membeship consistency. SPIN is found to be very powerful and easy to use without much knowledge of the formal verification process. GARP is well modeled in PROMELA, though it depends heavily on timers and multicasting, which are not directly supported in PROMELA.
Abstract This paper reports on an experience in formal verification using SPIN. The analyzed system is the Safety Logic of an interlocking system for the control of railway stations developed by Ansaldo. The Safety Logic is a process-based software architecture, which can be configured to implement different functions and control stations of different topology. In this paper we describe how a PROMELA model has been devised, which retains the configurability features of this architecture. Furthermore, we discuss the verification with SPIN of significant process configurations.
Abstract In this paper we present, illustrate, and discuss a number of techniques that can be used in the modeling and verification of electro-mechanical relay circuits. These techniques are based on state machine descriptions of circuits and their functions, and on applying validation tools for properties of such descriptions. In particular, we have applied tools that are based on the PROMELA language. There is also an html version of thispaper.
Abstract This paper discusses validation projects carried out for the Mobile Communication Division of Robert Bosch GmbH. We verified parts of their Mobile Communication Network (MCNet), a communication system which is to be used in infotainement systems of future cars. The protocols of the MCNet have been modeled in PROMELA and validated with SPIN. Apart from the validation results, this paper discusses some observations and recommendations of the use of PROMELA and SPIN.
Abstract An experimental verification tool has been developed to validate a microkernel. The goal was not to build a general purpose verification tool, but to experiment with specific aspects of the verification process. The system is similar to SPIN, but differs in a number of ways. Our experiment indicates that it is possible to develop a model checker in which the main functions of state generation, state storage and state analysis are clearly separated without sacrificing too much efficiency.
Spin Homepage