ODRES (output driven requirements engineering)method, which is being developed in the department of information systems comprises the following stages: separating out the context, specification of function results, specification of data sources, specification of data source processing, modelling, automatic projectionof interface of information system and prototype. While creating requirement specification, there arises a need to evaluate the quality of it. In every stage of creating requirement specification an analyst does not know if he or she has got enough information in order to do produce a working prototype of the system. Therefore, in this study the problem of information system is analysed, namely, the problem of how to hallmark the quality of ISRS? How to measure this quality? What must the IS be, so that it is of good quality? While seeking to evaluate the quality of RS, it is necessary to understant and analyse what is quality on the whole, how it is defined, how it is measured and if it is possible to measure it at all. In this study methods which are used to measure the quality and the possibilities of CASE tools to evaluate specification quality are analyzed. In the research requirements to evaluate the RS quality have also been established and the experiment that realizes the RS quality evaluation has been done.

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.

Šiuo metu egzistuoja įvairiausių sudėtingų sistemų imitacinių modelių kūrimo technologijų ir priemonių. Šiame darbe aiškinama, kaip imitacinis modelis gali būti integruojamas į verslo valdymo sistemą. Taip pat įvertinama, kad verlo valdymo sistemos gali būti paskirstytos atskiruose kompanijose ar kompiutersiuose. Šiame darbe bus išanalizuota koncepcija, kaip apjungti atskirus imitacinius modelius. Išanalizuota modelių integravimo į informacinę sistemą technologija. Pateikiami gamybos ir paskirstymo imitacinių modelių matematiniai aprašai, naudojant DEVS(Discrete Event Simulation) ir PLA(Piece-Linear Aggregates) specifikacijų metodus. / At present, a large number of modeling and simulation techniques and tools have been developed to deal with complex business systems. In this paper, we concentrate on scenario illustrating, how simulation models can be integrated in to business management system. Different infrastructure forms are possible, because services may be implemented on single machine or distributed throughout several companies’ networks. In this paper a concept will be analyzed - how to combine different simulation models. The technology for involvement of simulation models in to information systems will be created. Also the problem of simulation model transformation in to program code will be solved. For model formalization we can use a method of Piece-Linear Aggregates (PLA) that belongs to the class of time automata model. PLA method is close to Discrete Event Simulation (DEVS) formalism, which is used to create wide purpose simulation models.

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]