| Summary: | The ultimate goal of SPIN and indeed of all testing or validation methodology is to demonstrate, with a certain degree of confidence, that a proposed design or implementation meets its requirements. SPIN is a tool to simulate and validate Protocols. Promela, its source language, is a formal description technique like SDL and Estelle that is based on communicating state atomata. Unlike most other tools, SPIN is in the public domain and therefore is one of the most widely used formal verification tools today. Paper presents a formalization method of piece linear aggregates (PLA) and an investigation of possibilities to use SPIN system for validation of PLA specifications of distributed systems. It is shown that in order to write Promela specifications, processes used in the PLA model should be represented by finite state automata. PLA specification of two protocols, its description by finite state automata and its verification results in SPIN system are presented. It is shown in this paper that the SPIN system can be used for the verification of aggregate specifications. Using the SPIN system the finite state graphs of the processes used in the formal specification have to be formed. Then they have to be described in the Promela language.
|
|---|
