ИСПОЛЬЗОВАНИЕ ТЕХНИКИ «MODEL CHECKING » ДЛЯ ВЕРИФИКАЦИИ ПРОГРАММ ТЕРРИТОРИАЛЬНОГО РАЗВИТИЯ

Вега Висе Х. Л.

Аспирант, Кафедра системного анализа, Интитут вычислительной математики и информационных технологий, Казанский (Приволжский) Федеральный Университет

ИСПОЛЬЗОВАНИЕ ТЕХНИКИ «MODEL CHECKING » ДЛЯ ВЕРИФИКАЦИИ ПРОГРАММ ТЕРРИТОРИАЛЬНОГО РАЗВИТИЯ

Аннотация

Разработка программ территориального развития представляет собой сложную и важную задачу, которая требует тщательного рассмотрения многих аспектов. В процессе их создания некоторые важные аспекты остаются без должного внимания, что приводит к проблемам в реализации программ. Эти проблемы могут возникать, к примеру, из-за нехватки ресурсов или невыполнения сроков, установленных на первоначальном этапе планирования. Иногда под влиянием различных факторов главная цель проекта не может быть достигнута. Поэтому для обеспечения корректности и надежности операции системы возникает необходимость использовать некий инструмент, позволяющий гибко влиять на её производительность.

В настоящей статье рассматривается широко распространённый подход к моделированию и верификации систем, известный под названием Model Checking, позволяющий выявлять ошибки на разных этапах разработки и сопровождения программ территориального развития, чтобы последовательно устранять их.

Ключевые слова: программа территориального развития, model checking, темпоральная логика, CTL, NuSMV, Jetbrains MPS + mbeddr.

 Vega Vice J. L.

Postgraduate student,  Dept. of System Analysis, Institute of Computer Mathematics and Information Technologies, Kazan (Volga Region) Federal University

USE OF MODEL CHECKING FOR THE VERIFICATION OF TERRITORIAL DEVELOPMENT PROGRAMS

Abstract

The elaboration of territorial development programs is a complex and important task that requires the careful consideration of many aspects. Occasionally, during the creation process, some important aspects are overlooked, which leads to issues in the program. These issues can range from financial overdraft or failure to meet the established timeline, to failure to achieve the main objective of the program. Therefore, to ensure the correctness and reliability of the system, it is necessary to use a tool that allows for the flexibility to influence its performance.

This article discusses the widespread approach to the modeling and verification of systems, known as Model Checking, which allows for the detection of errors at different stages of the development and maintenance of territorial development programs in order to consistently eliminate them.

Keywords: territorial development program, model checking, temporal logic, CTL, NuSMV, Jetbrains MPS + mbeddr.

The elaboration of territorial development programs is a complex task that requires the careful consideration of many relational aspects, such as local resources and territorial indicators, as well as desired outcomes.

Programs are usually commissioned by government authorities, carried out by groups of experts that put in a lot of effort to complete the assigned task. Occasionally, because of the complexity of the projects, some inefficiency is built into the programs, and often, they manifest themselves much later, usually during the execution phase, when results are expected, therefore causing the program to fall short of expectations. _[1]

What can be done to fix this? A model verification technique known as Model Checking has played a decisive role in eliminating design errors in hardware and software, as well as other industrial processes _[1]. However, the author believes that the potential of this technique is not being fully utilized in the evaluation of development programs.

Model Checking is capable of automatically verifying the properties of a finite-state model, which is an abstraction of a real system, with the use of temporal logic expressions such as Linear Temporal Logic (LTL) or Computational Tree Logic (CTL) _[2] as a properties language, thus allowing the detection of inconsistencies long before the system is put into practice; in this case the system being a territorial development program.

Before the generalized use of Model Checking, errors were very common in many areas of advanced technology. Some of these errors were responsible for great capital loss as well as the loss of human lives. For example, many planes and space crafts were lost because of errors in the navigation system that went undetected at the time of conception. Another example would be the “friendly fire” incidents that were caused by the U.S. surface-to-air missile system, Patriot, in which at least one U.S. plane was destroyed.

Through the use of a model checker, for example, NuSMV _[3] or SPIN, it would be possible to define the abstract model using their modelling language; SMV or Promela, respectively. This way, it would be possible to emulate elements and behaviors of any development program, such as the resources that will be employed (financial, human, material, time), state of territorial indicators (economic-productive, sociocultural, ecological, institutional, etc.), the tasks and activities to be undertaken, as well as their interrelations according to the execution timeline along with their respective preconditions.

With the help of experts in a specific field, it’s possible to define how each element or behavior should affect each indicator, which would reflect on the model. Then, with the use of the temporal logic rules, we could check for the model properties at a given time, which would show if the applied changes to the territorial indicators produce the desired outcome. The author recommends the use of CTL _[4] for this purpose.

The author finds very interesting the idea of focusing the activities as concurrent, asynchronous processes that share and compete for common resources, utilizing the potential of parallel and distributed programming systems, which are included in the majority of model checkers. These processes would wait for the fulfillment of starting preconditions such as date or a specific state of one or more indicators, disputing and waiting for available common resources, for example, financial resources and personnel. On occasion these resources are pre-existent and in other cases they are the outcome of previous activities.

The following is an example of how the many territorial indicators interact with one another: imagine a city that has great potential for tourism, but suffers from high unemployment, which in turn leads to social problems that are detrimental to tourism, for example, crime and homelessness. The local government would like to fuel the development of tourism as a source of revenue, and use it to fix the unemployment problems in the area by utilizing the local inhabitants as the workforce behind the change. For this purpose, a plan is created for the training of the city inhabitants. Because this training demands a certain amount of time, any activities that would utilize the local workforce must take into consideration the time at which it would be ready. At the same time, these tasks cause many positive changes on territorial indicators such as economic development as a result of an increase in external revenue, the reduction of unemployment, and the betterment of the social situation. However, not all change would be positive; it’s very possible that the increase in tourism would also bring the destruction of the local nature in order to build hotels, golf courses, marinas and other touristic structures, thus having a negative impact on the city’s environmental indicators.

Another concept that must be considered is the meta-model, which, in this case would consist of the relationship between various models of territorial development programs at a macro level. For this concept, a strict regulation would be necessary for the coding and denomination during the modeling of resources, indicators, tasks, activities, etc.; this would allow them to interweave. This focus on seeing activities as asynchronous processes is reinforced when switching from independent models towards a unified meta-model.

Once at the meta-model level, or even at an independent model level, it can be very difficult to model directly using languages such as Promela or NuSMV; an alternative to this problem would be using a visual modeling tool. There are many tools that allow for the visual modeling of processes and systems; in some cases, this can be done utilizing activities diagrams of the standard UML, in other cases with a focus on business oriented processes of BPMN. However, these two ways lack the advantages of the Model Checking technique, therefore, in the great majority of cases, a combination of format transformations, as well as third party software would be needed in order to transform an activities diagram or any other kind of diagram into a comprehensible logical model to be verified through a model checker.

Nevertheless, there are other tools that maintain a focus on the potential of Model Checking from the beginning. An example that is not so well known to most specialists in this field, but that the author values greatly is JetBrains MPS (MetaProgramming System) with mbeddr, internally linked to NuSMV, joined as one computer system. Currently, this system is mainly implemented by German companies as well as companies from others European countries.

To conclude, it is the author’s opinion that through the use of the Model Checking technique it is possible to improve the creation of territorial development programs, which would employ the combination of JetBrains MPS + mbedded _[5] to define very complex finite-state models for the use of simulation and verifying both visually and through programming.

References

1. Karpov Y.G. Model Checking. Verifikaksia paralelnij i raspredelionnij programmnij sistem // BJV-Peterburg. – 2010; ISBN: 978-5-9775-0404-1. – P. 13-39.
2. Clarke E. M., Emerson E. A., Sistla, A. P. Automatic verification of finite-state concurrent systems using temporal logic specifications // ACM Transactions on Programming Languages and Systems. – 1986. - № 8(2). – P. 244-263.
3. Cavada R., Cimatti A., Jochim C. A., Keighren G., Olivetti E., Pistore M., Roveri M., Tchaltsev A. NuSMV 2.6 User Manual //Available: http://nusmv.fbk.eu/NuSMV/userman/v26/nusmv.pdf
4. Baier C., Katoen J.-P. Principles of model checking // Cambridge, MA: The MIT Press. – 2008; ISBN 978-0-262-02649-9. – P. 313-447.
5. Rosenberger, Ch. Model Checking for State Machines with mbeddr and NuSMV // Available: http://mbeddr.com/files/modelcheckingforstate-machineswithmbeddrandnusmv.pdf