Глава
VERMONT - a toolset for checking SDN packet forwarding policies on-line
Характерная особенность моделей Крипке и большинства темпоральных логик (PLTL, CTL, PDL, mu-исчисление и др.), используемых в качестве формальных языков спецификации, состоит в том, что элементарные свойства вычислений зависят только от состояний модели, но не от вычислений, которыми достигаются состояния. Однако для стороннего наблюдателя поведение реагирующей системы проявляется в соответствии между последовательностями стимулов (сигналов), которыми внешняя среда воздействует на систему, и откликов (действий), которые вырабатывает или исполняет система в ответ на внешние воздействия. Поэтому при верификации некоторых видов реагирующих систем элементарными свойствами становятся множества конечных последовательностей действий. Это обстоятельство должно быть также учтено при разработке формального языка спецификаций поведения таких систем. В данной статье рассмотрена задача формальной верификации реагирующих систем, моделируемых конечными автоматами-преоб\-разователями. Для спецификации их поведения предложен новый вариант темпоральной логики линейного времени LTL-FL (LTL with Formal Languages). Формальные языки (множества конечных слов фиксированных алфавитов) в формулах LTL-FL используются для представления элементарных свойств вычислений, а также для параметризации темпоральных операторов. Установлено, что задача проверки выполнимости формул регулярного фрагмента FL-LTL на конечных автоматах преобразователях разрешима.
This volume contains the papers presented at CS&P 2014: 23th International Workshop on Concurrency, Specification and Programming held on September 28 - October 1, 2014 in Chemnitz. Since the early seventies Warsaw University and Humboldt-University have alternately organized an annual workshop - since 1993 as CS&P. Over time, it has grown from a bilateral seminar to a meeting attended also by colleagues from other countries than Poland and Germany. This year there are 34 participants from 10 countries.
This paper regards problems of analysis and verification of complex modern operating systems, which should take into account variability and configurability of those systems. The main problems of current interest are related with conditional compilation as variability mechanism widely used in system software domain. It makes impossible fruitful analysis of separate pieces of code combined into system variants, because most of these pieces of code has no interface and behavior. From the other side, analysis of all separate variants is also impossible due to their enormous number. The paper provides an overview of analysis methods that are able to cope with the stated problems, distinguishing two classes of such approaches: analysis of variants sampling based on some variants coverage criteria and variation-aware analysis processing many variants simultaneously and using similarities between them to minimize resources required. For future development we choose the most scalable technics, sampling analysis based on code coverage and on coverage of feature combinations and variation-aware analysis using counterexample guided abstraction refinement approach.
Workshop on Program Semantics, Specifi cation and Verifi cation: Theory and Applications is the leading event in Russia in the fi eld of applying of the formal methods to software analysis. Proceedings of the fourth workshop are dedicated to formalisms for program semantics, formal models and veri cation, programming and speci fication languages, etc.
Nested Petri nets is an extension of Petri net formalism with net tokens for modelling multi-agent distributed systems with complex structure. Temporal logics, such as CTL, are used to state requirements of software systems behaviour. However, in the case of nested Petri nets models, CTL is not expressive enough for specification of system behaviour. In this paper we propose an extension of CTL with a new modality for specifying agents behavior. We define syntax and formal semantics for our logic, and give small examples of its usage.
В работе предлагается метод автоматизированного построения поведенческих моделей микропроцессоров, используемых при генерации тестовых программ для предсказания результатов их выполнения. Предложенный метод основан на использовании формальных спецификаций системы команд. Данный метод реализован в инструменте MicroTESK, разработанном в ИСП РАН. Инструмент успешно применяется для верификации промыш- ленных микропроцессоров.
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.