GLOBDATA is a project that aims to design and implement a middleware tool offering the abstraction of a global object database repository. This tool, called COPLA, supports transactional access to geographically distributed persistent objects independent of their location. Additionally, it supports replication of data according to different consistency criteria. For this purpose, COPLA implements a number of consistency protocols offering different tradeoffs between performance and fault-tolerance. This paper presents the analysis of one of two strong consistency protocols for the GLOBDATA system, the voting protocol. A protocol relies heavily on the use of atomic translation primitive as a building block to serialize conflicting transactions. The paper presents an in-depth description of the conceptual model using UML-based analysis of the protocol which later is used to define the PLA (piece-linear aggregates) model of the system, a discrete event-based simulation of the processes. As a result of the work, the PLA model is ready to be used to validate, verify and simulate various behavioral and performance characteristics of the model using mathematical proof techniques.

Formalios specifikacijos – tai matematinis programinės ar techninės įrangos aprašymas, kurį galima naudoti sistemos realizacijai. Formalių specifikacijų naudojimas dar negarantuoja specifikacijos teisingumo. Tam naudojami formalaus verifikavimo metodai. Šiame dokumente aptariami formalių specifikacijų validavimo metodai. Du populiaraiausi formalių specifikacijų validavimo metodai yra pasiekiamų būsenų grafo analizė bei invarianto tikrinimas. Pasiekiamų būsenų grafo analizę sudaro pasiekiamų būsenų grafo generavimas ir analizė. Grafo analizės metu ieškoma aklaviečių, uždarų ciklų, nepasiekiamų būsenų, atliekamas būsenų koordinačių apribojimų tikrinimas bei invarianto tikrinimas. Tradiciniai pasiekiamų būsenų grafo sudarymo algoritmai grafo sudarymui naudoja sistemos būsenų eilę. Kiekviena išanalizuota būsena įrašoma į pasiekiamų būsenų grafą. Dokumente aptariamas lygiagretaus programavimo naudojimas būsenų grafo generavimui, kuris analizuoja ir generuoja sistemos būsenas naudodamas lygiagrečias gijas. Eksperimentų su vienkanale aptarnavimo sistema metu nustatyta, kad lygiagretaus algoritmo naudojimas šio uždavinio metu leidžia pagerinti sistemos veikimą iki 35%, priklausomai nuo būsenų skaičiaus. / Arguably the most important task in creation of software is user requirement specification. Accurate requirement specification allows avoidance of errors in late stages of software development. This is extremely important in critical systems, where even vague error can cause great financial losses or even human victims. One of the methods used for precise user requirement specification is use of formal specifications. Formal specification is a mathematical method for describing of software or hardware, which might be suitable for system realization. Nevertheless, the construction of formal specifications does not guarantee the correctness of specification. For this reason formal specification validation is necessary. In this paper methods of formal specification validation are discussed. Two most popular methods of formal specification validation are reachable state graph analysis and invariant checking. Reachable state graph analysis consists of graph generation and graph analysis. Graphs can be analyzed for dead-ends, closed loops, state reach ability checking, coordinate restriction checking or invariant checking. Traditional reachable graph generation algorithm uses unanalyzed states queue to produce reachable state graph. Each step single state is analyzed and depending on results new vertex or edge is added to state graph. An improvement to the algorithm to consider is usage of parallel programming to process multiple states simultaneously. This allows increasing the... [to full text]