Wyniki wyszukiwania - BazTech

Ograniczanie wyników

2 Przegląd Elektrotechniczny

Znaleziono wyników: 2

Liczba wyników na stronie

Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych: Bogor

Sortuj według:

Ogranicz wyniki do:

A Framework to Automatic Deadlock Detection in Concurrent Programs

Mahdian F., Rafe V., Rafeh R.

Przegląd Elektrotechniczny

2012

R. 88, nr 1b

182-184

Nowadays, concurrency is one of the most common features of software systems. In such systems, different parts of the system either are working together or separately. In these cases, deadlock is a common defect. In many systems –especially safety critical ones- deadlock is a serious problem. Hence, it is very important to find them before deploying the system. Since model checking is an accurate mechanism to automatically verify software and hardware systems, using this technique is a proper solution to automatic deadlock detection. In this paper, we present an approach to automatic deadlock detection using Bogor – a well known model checker. To do so, at first, we determine global variables, shared resources and in general, all parts that may cause a deadlock. Then, we translate them to BIR – the input language of the Bogor. Bogor generates the transition system and shows that if there is any deadlock in the program. In the cases in which Bogor finds a deadlock, it shows a counter example to help programmers to fix the problem. To illustrate all the main concepts of the approach, we use different concurrent Java programs as case studies.

oprogramowaniu charakteryzującym się zgodnością różne części mogą pracować niezależnie lub wspólnie. Największym problemem w tego typu programach jest stan zakleszczenia (deadlock). Dlatego ważne jest stworzenie mechanizmu automatycznego wykrywania takiej sytuacji. W artykule opisano metodę Bogor, w tym także BIR – język wejściowy do Bogor.

Formal Analysis of Service-oriented Architectures

Rafe V.

Przegląd Elektrotechniczny

2011

R. 87, nr 11

310-313

Even though model checking is one of the most accurate analyses techniques to verify software systems, the problem of model checking is that it is not feasible for large and complex software systems, which their state spaces are too large. In these situations one can use scenariobased model checking techniques. In this paper, we present an approach to analyze large and complex systems specified by graph transformation systems. To do so, we propose the scenario-based model checking techniques. We explain how the approach will affect to the size of the state space by focusing on the most important occurring scenarios in a system.

Problem sprawdzania modelu software jest istotny jeśli badamy duży i złożony system. W artykule zaprezentowano metodę umożliwiającą taką analizę systemu opisanego przez transformację grafu. Zaproponowano technikę sprawdzania opierającą się na modelu bazującym na scenariuszu.