|
ИСТИНА |
Войти в систему Регистрация |
ИПМех РАН |
||
Projecting Transition Systems: Overcoming State Explosion in Concurrent System Verificationстатья
Информация о цитировании статьи получена из
Web of Science,
Scopus
Статья опубликована в журнале из списка Web of Science и/или Scopus
Дата последнего поиска статьи во внешних источниках: 11 января 2016 г.
- Автор: Kamkin A.S.
- Журнал: Programming and Computer Software
- Том: 41
- Номер: 6
- Год издания: 2015
- Издательство: Pleiades Publishing, Ltd
- Местоположение издательства: Road Town, United Kingdom
- Первая страница: 311
- Последняя страница: 324
- DOI: 10.1134/S0361768815060043
- Аннотация: The paper introduces a method for overcoming state explosion arising when verifying concurrent and distributed computer systems. The method is based on projecting a system state space onto a number of subspaces associated with quite small and, generally speaking, overlapping groups of processes. Analysis of the system—checking whether a given property holds on the system states—is carried out by collaborative exploration of the projections’ state graphs; the process is completed as soon as all transitions of all projections have been traversed (usually, this requires significantly less amount of time than exploring the state graph of the entire system). To increase controllability of the traversing process, it is suggested to use techniques for cooperative searching paths in the projections (the latter may appear to be highly nondeterministic due to the loss of information upon projecting). In this work, certain issues of the introduced verification scheme are investigated, and results of some experiments are given. The method described can be applied to model checking, as well as to model-based testing, namely for automatic test sequence generation.
- Добавил в систему: Камкин Александр Сергеевич