Глава
A High-Level Framework for Distributed Systems with Simulation-Based Testing Support
В книге
Mногоуровневые мультиагентные системы (МАС) с динамической структурой широко используют- ся при решении важных прикладных задач в телекоммуникационных, транспортных, социальных и других системах. Поэтому обеспечение корректности таких систем является актуальной и значимой задачей. Одним из самых уязвимых для ошибок этапов разработки системы в рамках модельно- ориентированного подхода является этап реализации, на котором по разработанной модели строит- ся программный код. В данной работе представлен алгоритм автоматической трансляции моделей МАС в виде вложенных сетей Петри в системы распределенных компонентов. Вложенные сети Пет- ри являются расширением сетей Петри в рамках подхода “сети внутри сетей”, когда фишки в сети Петри сами могут являться сетями Петри, обладать автономным поведением и взаимодействовать с другими фишками сети. Это позволяет естественным образом моделировать МАС с динамической структурой. Представленная в работе трансляция сохраняет уровень распределенности и важные поведенче- ские свойства исходной модели (безопасность, живость, условная живость), а также обеспечивает справедливость исполнения целевой системы. Использование такой трансляции позволяет авто- матизировать построение распределенных МАС по моделям вложенных сетей Петри. В качестве апробации трансляция вложенных сетей Петри в распределенные системы компонентов была реа- лизована на основе компонентной технологии EJB.
Coordination of several distributed system components is an error-prone task, since interaction of several simple components can generate rather sophisticated behavior. Verification of such systems is very difficult or even impossible because of the so-called state space explosion problem, when the size of the system reachability set grows exponentially on the number of interacting agents. To overcome this problem several approaches to construct correct models of interacting agents in a compositional way were proposed in the literature. They define different properties and conditions to ensure correct behavior of interacting agents. Checking these conditions may be in its turn quite a problem. In this paper, we propose patterns for correct composition of component models. For justifying these patterns we use special net morphisms. However, to apply patterns the user does not need to be familiar with the underlying theory.
Checking the correctness of distributed systems is one of the most difficult and urgent problems in software engineering. A combined toolset for the verification of real-time distributed systems (RTDS) is described. RTDSs are specified as statecharts in the Universal Modeling Language (UML). The semantics of statecharts is defined by means of hierarchical timed automata. The combined toolset consists of a UML statechart editor, a verification tool for model checking networks of real-time automata in UPPAAL, and a translator of UML statecharts into networks of timed automata. The focus is on the translation algorithm from UML statecharts into networks of hierarchical timed automata. To illustrate the proposed approach to the verification of RTDSs, a toy example of a real-time crossroad traffic control system is analyzed.