Return to search

Agregatinių specifikacijų verifikavimas transformuojant jas į baigtinius automatus / Verification of Aggregate specifications transforming them in to finite-state automata

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.

Identiferoai:union.ndltd.org:LABT_ETD/oai:elaba.lt:LT-eLABa-0001:E.02~2006~D_20060605_231233-92570
Date05 June 2006
CreatorsBaužaitė, Rasa
ContributorsJasinevičius, Raimundas, Mikuckas, Antanas, Barauskas, Rimantas, Telksnys, Laimutis, Maciulevičius, Stasys, Plėštys, Rimantas, Mockus, Jonas, Pranevičius, Henrikas, Kaunas University of Technology
PublisherLithuanian Academic Libraries Network (LABT), Kaunas University of Technology
Source SetsLithuanian ETD submission system
LanguageLithuanian
Detected LanguageEnglish
TypeMaster thesis
Formatapplication/pdf
Sourcehttp://vddb.library.lt/obj/LT-eLABa-0001:E.02~2006~D_20060605_231233-92570
RightsUnrestricted

Page generated in 0.0021 seconds