Исследователь
Researcher
Большое пространство состояний программ затрудняет или делает невозможной их непосредственную верификацию методом проверки модели (model checking). Наличие симметрии в программе достаточно часто позволяет упростить модель и сократить её пространство состояний, что приводит к значительному снижению времени верификации. Классический подход состоит в обнаружении группы симметрии и построении на её основе фактормодели — упрощённой модели для верификации. Однако не все инструменты имеют поддержку симметрии, а инструменты с такой поддержкой не всегда справляются с поставленной задачей, так как поиск подходящей группы симметрии является вычислительно сложной задачей.
В работе предлагается альтернативный классическому подход к разработке программ, основанный на явном выделении симметрии. В программе выделяется ядро — координационный центр, который работает с учётом симметрии и отвечает за выполнимость заданных темпоральных свойств. Ядро координирует вычисления, вынесенные за его пределы — в обвязку ядра. В связи с этим ядро имеет небольшое пространство состояний, заменяет собой фактормодель и может быть верифицировано инструментом проверки модели без поддержки симметрии. Обвязка не может вмешиваться в работу верифицированного ядра и нарушать его свойства. Подход продемонстрирован на примере разработки и верификации арбитра ресурсов марсохода. Арбитр координирует доступ n процессов к m ресурсам, где n и m — натуральные числа. Используются язык программирования C/C++ и инструмент проверки модели Spin. Модель поведения ядра автоматически извлекается верификатором Spin из C-кода. Проверке подлежат темпоральные свойства, выраженные с помощью линейной темпоральной логики LTL.
The large states pace of programs makes their direct verification by model checking difficult or impossible. The presence of symmetry in a program often allows simplifying the model and reducing its state space, leading to significant decrease of verification time. The classical approach consists in detecting a symmetry group and constructing a quotient model based on it — a simplified model for verification purposes. However, not all tools provide support for symmetry, and those that do may still struggle because finding an appropriate symmetry group is computationally complex problem.
This work proposes an approach to program development based on explicit symmetry exploitation, which is an alternative to the classical one. In the program, a core is extracted — a coordination center working under consideration of symmetry and responsible for ensuring temporal properties. The core coordinates computations outside itself — those placed in the wrapper surrounding the core. As a result, the core has a small state space, replace the quotient model and allows verification using a model checker without symmetry support. The wrapper cannot interfere in the operation of the verified core and violate its properties. The approach is demonstrated by the example of the development and verification of the Mars rover resource arbiter. The arbiter coordinates access of n processes to m resources where both n and m are natural numbers. Programming languages C/C++ and the Spin model checker tool are used. The behavioral model of the core is automatically extracted by the Spin tool from the C code. Temporal properties expressed via Linear Temporal Logic (LTL) are subject to verification.
The authors declare that there are no conflicts of interest present.