Wyniki wyszukiwania - BazTech

Ograniczanie wyników

2 Annals of Computer Science and Information Systems

Znaleziono wyników: 2

Liczba wyników na stronie

Wyniki wyszukiwania

Sortuj według:

Ogranicz wyniki do:

An Experimentation Framework for Specification and Verification of Web Services

Katra Szymon, Daszczuk Wiktor, Czejdo Danny

Annals of Computer Science and Information Systems

2022

Vol. 30

913--917

Designing and implementing Web Services constitutes a large and constantly growing part of the information technology market. It requires efficient personnel training in the application's preparation (visual programming, libraries, repositories, code reusability) and other stages of development, such as formal verification. Web Services have specific scenarios in which distributed processes and network resources are used. This aspect of services requires integration with the model checkers. This article presents the experimentation framework in which services can be specified and then formally analyzed against deadlock-freedom, achievement of process goals, and similar features. This language enriches the basic Rybu language with the ability to use variables in processes, service calls between servers, new structural instructions, and other constructions known to programmers while remaining in line with declarative, mathematical IMDS formalism. Additionally, the development environment allows simulation of a counterexample or a witness - obtained as a result of the model checking - in a similar way to traditional debuggers.

Threefold analysis of distributed systems: IMDS, Petri net and distributed automata DA3

Daszczuk Wiktor

Annals of Computer Science and Information Systems

2017

Vol. 13

377--386

Integrated Model of Distributed Systems is used to model and verify distributed systems. In the formalism, a system is modeled as a set of servers' states and agents' messages. The operation of a system is modeled as actions converting global system configuration (a set of states and messages) to a new configuration. The formalism is used in Dedan verification environment, in which specification and verification of distributed systems is performed. For the graphical specification and simulation of distributed systems, Distributed Autonomous and Asynchronous Automata (DA3) are invented. Such simulation does not require calculation of global configuration space of a system. Two forms of DA3 are shown: Server-DA3 (SDA3) for the server view and Agent-DA3 (ADA3) for the agent view.