Глава
Dynamic Composition and Analysis of Modern Service-Oriented Information Systems
В книге
Характерная особенность моделей Крипке и большинства темпоральных логик (PLTL, CTL, PDL, mu-исчисление и др.), используемых в качестве формальных языков спецификации, состоит в том, что элементарные свойства вычислений зависят только от состояний модели, но не от вычислений, которыми достигаются состояния. Однако для стороннего наблюдателя поведение реагирующей системы проявляется в соответствии между последовательностями стимулов (сигналов), которыми внешняя среда воздействует на систему, и откликов (действий), которые вырабатывает или исполняет система в ответ на внешние воздействия. Поэтому при верификации некоторых видов реагирующих систем элементарными свойствами становятся множества конечных последовательностей действий. Это обстоятельство должно быть также учтено при разработке формального языка спецификаций поведения таких систем. В данной статье рассмотрена задача формальной верификации реагирующих систем, моделируемых конечными автоматами-преоб\-разователями. Для спецификации их поведения предложен новый вариант темпоральной логики линейного времени LTL-FL (LTL with Formal Languages). Формальные языки (множества конечных слов фиксированных алфавитов) в формулах LTL-FL используются для представления элементарных свойств вычислений, а также для параметризации темпоральных операторов. Установлено, что задача проверки выполнимости формул регулярного фрагмента FL-LTL на конечных автоматах преобразователях разрешима.
Рассматриваются основные положения комплексного метода для оценки инвестиционной привлекательности IT-проектов. Отмечено, что в данный момент широко распространена архитектура на основе сервисов (СОА). Среди современных работ, учитывающих архитектуру СОА в методики оценки экономической эффективности ИС, выделен подход, основанный на расширении EPC.
This book constitutes the proceedings of the 9th International Workshop on Enterprise and Organizational Modeling and Simulation, EOMAS 2013, held in conjunction with CAiSE 2013 in Valencia, Spain, in June 2013.
Tools and methods for modeling and simulation are widely used in enterprise engineering, organizational studies, and business process management. In monitoring and evaluating business processes and the interactions of actors in a realistic environment, modeling and simulation have proven to be both powerful, efficient, and economic, especially if complemented by animation and gaming elements.
The ten contributions in this volume were carefully reviewed and selected from 22 submissions. They explore the above topics, address the underlying challenges, find and improve solutions, and show the application of modeling and simulation in the domains of enterprises, their organizations and underlying business processes.
В статье проведено исследование операционных рисков в рамках сервисного подхода создания информационных систем (ИС) и предложен подход к их классификации, основывающийся на ошибках систем, которые являются поставщиками сервисов для типового приложения с сервисно-ориентированной архитектурой. С использованием предложенной классификации собрана статистика сообщений об ошибках за 5 лет по двум предприятиям нефтегазовой и металлургической отрасли. Проведен опрос экспертов с целью определения убытков от исследованных рисков и приведена оценка возможного урона.
В статье в качестве формальной модели последовательных реагирующих систем была предложена модель вычислений конечных автоматов-преобразователей, работающих над полугруппами действий. Для спецификации поведений таких автоматов был предложен специальный вариант темпоральной логики линейного времени LTL-FL (LTL with Formal Languages). Формальные языки (множества конечных слов фиксированных алфавитов) в формулах LTL-FL используются для параметризации темпоральных операторов. В этой же статье было показано, что задача проверки выполнимости формул регулярного фрагмента FL-LTL на конечных автоматах преобразователях, работающих над свободными полугруппами, разрешима со сложностью по времени, оцениваемой двойной экспонентой от размера проверяемой формулы.
This book constitutes the proceedings of the 35th International Conference on Application and Theory of Petri Nets and Concurrency, PETRI NETS 2014, held in Tunis, Tunisia, in June 2014. The 15 regular papers and 4 tool papers presented in this volume were carefully reviewed and selected from 48 submissions. In addition the book contains 3 invited talks in full paper length. The papers cover various topics in the field of Petri nets and related models of concurrency.
В данной статье рассказывается об изучении колорита в акварельной живописи. Для создания выразительного образа художник выбирает среди цветов реального мира только те, которые соответствуют его мыслям, чувствам и художественному решению живописной работы. Приводятся примеры заданий, способствующих изучению колорита в акварельной живописи и благоприятно влияющие на развитие творческих способностей, образного мышления студентов, учащихся и школьников.
This volume constitutes the refereed proceedings of the 37th International Symposium on Mathematical Foundations of Computer Science, MFCS 2012, held in Bratislava, Slovakia, in August 2012. The 63 revised full papers presented together with 8 invited talks were carefully reviewed and selected from 162 submissions. Topics covered include algorithmic game theory, algorithmic learning theory, algorithms and data structures, automata, formal languages, bioinformatics, complexity, computational geometry, computer-assisted reasoning, concurrency theory, databases and knowledge-based systems, foundations of computing, logic in computer science, models of computation, semantics and verification of programs, and theoretical issues in artificial intelligence.