The problem of analyzing concurrent systems has been investigated by many researchers, and several solutions have been proposed. Among the proposed techniques, reachability analysis—systematic enumeration of reachable states in a finite-state model—is attractive because it is conceptually simple and relatively straightforward to automate and can be used in conjunction with model-checking procedures to check for application-specific as well as general properties. The system validation problem considered here is the problem of verifying that the original specification is itself logically consistent. If, for instance, the specification has a design error, an implementation is expected to pass a conformance test if it contains the same error. A validation for the logical consistency of the system, however, must reveal the design error. 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 the existing validation techniques and methods. Specified and analyzed systems are presented as reachable state graph. The implementation of the aggregate specifications validation system is also presented.

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]

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]