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.

Darbe nagrinėjamas realiojo laiko sistemų, specifikuotų agregatiniu metodu, verifikavimo uždavinys. Sprendžiant šį uždavinį, naudojama pasiekiamų būsenų grafo sudarymo metodika, leidžianti įvertinti laiko intervalus, kuriais įvyksta sistemoje apibrėžti įvykiai. Darbe nagrinėjami pasiekiamų būsenų grafo sudarymo algoritmai ir pateikta prototipinėse programose naudojama duomenų struktūra. Suformuluoti ir įrodyti teiginiai apie pasiekiamų būsenų grafo sudarymo algoritmo sudėtingumą (maksimalaus vienos būsenos galimų perėjimų skaičiaus; grafo viršūnių skaičiaus augimo priklausomybės nuo įvykių skaičiaus; maksimalaus įvykių skaičiaus elgsenoje laiko intervale; maksimalaus viršūnių skaičiaus laiko intervale.) Pateikta trijų testinių sistemų grafų automatizuoto sudarymo analizė. Parodyta, kad Simplekso optimizavimo procedūra laiko momentų palyginimui gali būti naudojama tik atskirais atvejais. / The work deals with a verification task of real time system specified by aggregate method. While solving the task, a technique for creation a reachable state graph is used. The technique permits to evaluate intervals of time when the defined system events occur. Reachable state graph creation algorithms are analysed in the work. A data structure used in prototype software is presented in the work too. Assertions about a complexity of algorithm for reachable state graph creation are formulated and proved. These assertions concern maximum number of transitions from single state, dependency of number of graph verteles growth on a number of events, maximum number of events in a behaviour during time interval, and maximum number of vertexes during time interval. Analysis of automated creation of graphs for three test systems is presented. It is shown that Simplex optimisation procedure for comparison of time intervals can be used only in certain cases.

This work presents business process analysis methodology which consists of presentation of the business processes created on the ground of the Resource Event Agent model by means of Piece–Linear Aggregate approach. The aggregate specification is analyzing using first order predicate logic while checking correctness by resolution method using logic programming based language Prolog. The work is concluded with concrete example of analysis of Resource Event Agent model based business process using the aggregate approach. The novelty of this work PLA (Piece-Linear Aggregate) model and the software tools, created on the ground of PLA (Piece-Linear Aggregate), are used the first time for business processes analysis that is defined using REA formalism. The use of such integrated models allows performing the automated analysis of general and individual properties (completeness, deadlock freeness, termination or cyclic behavior, boundedness) of defined business processes. The main results are achieved: • The methodology, that consists of presentation of the business processes created on the ground of the Resource Event Agent model by means of Piece–Linear Aggregate approach. • Verification and validation of general and individual properties by using PLA and PROLOG language approach designed system that executes the analysis of aggregate specification. • Implementing internal accounting controls as constraints in relational algebra, SQL and PROLOG language. • Concrete... [to full text]