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.

It is notoriously difficult to define, or even to understand, the behavior of a system of interacting asynchronous processes. Improbable sequences of events that lead to errors are easily overlooked by a protocol designer. If such errors occur in practice, they will be virtually irreproducible and very hard to fix. A distinct advantage of an automated validator is that it has no preconceived notions about what is meant or what is likely in a protocol definition: it examines possibilities not probabilities. It can patiently perform the analysis for millions of cases, faster and more accurately than could ever be done by hand. An automated analysis of all reachable states in a distributed system can be used to trace obscure logical errors that would be very hard to find manually. This type of validation is traditionally performed by the symbolic execution of a finite state machine model of the system studied. The author presents an overview of existing validation techniques and methods. The implementation of Aggregate specification safety and livenes is also presented: described safety and livenes properties, algorithms and implementation. Described experiments with system, and results compared with world-famous validation system SPIN. Performance of implemented algorithms evaluated. Given some suggestions for further development of automated aggregate specification validation system.

Web services provide means to computerize e-business processes. To be able to satisfy business requirements web services must be developed rapidly and in high quality. Code generation techniques are frequently employed. In such context, verification of web service models emerges as a relevant issue: model verification makes it easier to detect and remove errors of system specification at the early stages of software development cycle. Available model verification tools require transformation of the objective model into complex formal notations, supported by the tool. It would be convenient to implement model verification directly in a CASE tool. This thesis describes a method for checking web service models based on verification of UML state machines. Conceptual algorithms for checking state machine’s safety criteria: reachability, completeness and consistency are provided. These algorithms, implemented in CASE tools could help to ensure the correctness and consistency of behavioral models. Also, a state machine template for composite web services is presented. Template complements state machine with transitions representing unsuccessful scenarios. Designer is freed from necessity to repeat reoccurring unsuccessful transitions for every event. This template is useful for automatic code generation.

In this work was studying literature related to object orientated programming tools for hardware design, capabilities for modeling and synthesis of high-level models of abstraction. It was founded-out the operating principles of high-speed bus and created prototype of such bus in TLM level. It was created methodology for transformation of high-speed bus prototype to RTL level. This methodology was used for transformation of high-speed bus prototype to RTL level. Transformed module was synthesized to gate level. Simulation speed of high-speed bus model in TLM was compared with simulation speed of model in behavioral level. It was demonstrated universality and reuse capabilities of TLM models.

Integrated circuit (IC) layer topology analysis methods are the main research topic of this doctoral thesis. Multiple methods are presented for IC layer feature analysis along with a software system where they are implemented and tested. Each of different IC layers has distinct features therefore it is very difficult to use universal algorithm for their analysis. A specialized software system was developed to test various analysis algorithms. The system and its architecture is a part of this thesis. Main tasks solved during research of this these were: finding or developing of optimal methods suitable for IC layer structure recognition, software system design and implementation, experimental testing of implemented methods accuracy and efficiency. Thesis consists of introduction, four chapters and the chapter of conclusions. In the introduction scientific novelty of the work is described as well as the aims and tasks of the work are formulated and the author’s publications and structure of the thesis are presented. The first chapter is dedicated to literature review. It covers existing IC layer structure analysis systems and algorithms which are used for this task. Generic image processing and analysis algorithms and methods are also covered as they are used as part of methodology developed in this thesis. The second chapter details different types of IC layers and their properties. Image processing and analysis methods suitable for each of these layer types are... [to full text] / Disertacijoje nagrinėjama integrinių grandynų (IG) topologijos elementų atpažinimo sistemos metodai ir algoritmai, jų taikymas bei pačios sistemos architektūra. Integrinių schemų projektavimo ir gamybos pramonėje problema yra automatinis kiekvieno technologinio lusto sluoksnio vaizdinės informacijos apdorojimas ir analizė, tiksliai išskiriant gamybos proceso metu suformuotas struktūras, tam kad šių duomenų pagalba galima būtų atlikti gamybos proceso tikslumo patikrinimą. Šio disertacijos darbo tyrimų objektas yra puslaidininkinių integrinių schemų sluoksniuose suformuoti elementai. Kiekvieno iš skirtingų sluoksnių struktūros pasižymi skirtingomis savybėmis, todėl labai sunku sukurti universalius analizės metodus. Dėl šios priežasties buvo sukurta speciali programinės įrangos (PĮ) sistema. PĮ architektūra yra disertacijos tyrimų objektas. Pagrindiniai disertacijoje sprendžiami uždaviniai: IG elementų struktūrų atpažinimo metodų pritaikymas ir kūrimas, PĮ sistemos projektavimas ir įgyvendinimas, eksperimentinis įdiegtų metodų efektyvumo ir tikslumo tyrimas. Disertaciją sudaro įvadas, keturi skyriai ir rezultatų apibendrinimas. Įvade nagrinėjamas problemos aktualumas, formuluojamas darbo tikslas bei uždaviniai, aprašomas mokslinis darbo naujumas, pristatomi autoriaus pranešimai ir publikacijos, disertacijos struktūra. Pirmasis skyrius skirtas analitinei literatūros apžvalgai. Jame nagrinėjamos žinomos IG topologijos elementų atpažinimo sistemos ir jose naudojami metodai... [toliau žr. visą tekstą]