Another projects with application of symbolic technology:
1. “Formalization and Processing of Legal Requirements” (formalization of regulations, smart contracts for cryptocurrency market)
The project has been started together with the Glushkov Institute of Cybernetic and the Kherson State University in 2013.
The legal requirements and laws of different countries of European Union and associated members of EU intersect one with each other during the international financial transactions and agreements. Understanding of legal requirements in the scope of international agreements plays the important role for avoiding of inconsistencies and misuse of ambiguity. Taxation offices and courts of different countries can miss the legal violation or misinterpret the legal case and admit wrong verdict. Different fraud schemes can be hidden and hard to recognize.
One of the ways to avoid such issues is the creation of formal model of legal requirements and to provide the corresponding processing and algebraic modeling of legal requirements with the purposes of checking of consistency and compliance of transactions with the laws of corresponding countries.
The main goal of the project is to join together formal methods and contemporary deductive facilities for analysis and processing of the real legal documents. The additional goal is to use formal legal requirements in the simulation of financial transactions and agreements implementation for providing the financial security and avoiding violations and fraud schemes.
It is anticipated that team of law experts and algebraists works with legal requirements documents together for the creation of formal model. The formalization is to transform the behavioral requirements to expressions of behavior algebra and non-behavioral statements as first-order logic axioms. The general purpose of the project is to create the technology of manual, semi-manual or automatic methods of formalization. The corresponding assistant software will be created for automatic purposes. The technology should include the usage of world legal ontology and transforming the acknowledge into algebraic specifications. The result is the set of models of legal requirements presented as behavior algebra specifications.
The created formal model of legal requirements is the input for algebraic programming system or other deductive tools. In the scope of the algebraic system, the number of properties could be checked. There are the properties of consistency and completeness of legal requirements items, compliance with the legal documents of the high level of abstractions especially Constitution.
All this shall be implemented in computations of algebraic systems.
The specific of algebraic research is that we face with big data and big complexity with specific formalization. So, all powerful modern algebraic methods like invariant generation, IC3 technology, approximation methods shall be applied. The corresponding specific technology for modeling and processing of legal requirements shall be set based on the possibilities of the algebraic system.
Concept of “Digital Taxation Office”
It is anticipated the creation of an experimental network of clients that communicate with algebraic systems. Clients perform the different financial transactions and conclude the agreements. The agreements between clients created in the algebraic form like the formalization of legal requirements. The algebraic system with the formal model of Tax Code and other regulations check transactions and agreements for compliance and detect the violation.
Financial Security
Usage of formal methods can avoid and detect the schemes of fraud. Known different cases of fraud shall be formalized as algebraic specifications and the system could detect such cases in the transaction. The search of such cases is implemented as resolving of equations in behavior algebra. One of the intentions of such research is combining of the system with cryptocurrency market.
The project is in progress and will be continued in the scope of Horizon 2020.
For more detail, see our conference paper (presentation):
2. Verification and Testing of Cyber-Physical Systems
The project has been started in Glushkov Institute of cybernetics in 2019. It considers the analysis and verification of a logistic system that integrates different devices for control of cargo and the Internet of Things. It uses the behavior algebra methods for formalization and analysis of such systems.
The paper will be uploaded in May.
3. “Cyber-physical systems. Biology models”
The project has been started together with the Glushkov Institute of Cybernetic in 2017. The main goal of the project is to provide the analysis, reachability of properties and symbolic simulation of biology models. It anticipates developing of formal methods based on the hybrid modeling (composition of discrete and continuous behavior). The theory of semi-group modeling in the scope of behavior algebra proposed by academician A.Letichevsky (senior) is used in the research. This project is in the initial stage and it is anticipated to develop the row of the examples of models of membrane transport, gene regulations and biochemical analysis.
4. “Internet of Things. Control System of Network of Medical Portable Devices”
The project has been initiated together with Pharmacologist company “Yuria Farm” and the Institute of Cybernetics. The aim of the project is to organize the gathering from portable medical devices to the system and to create the model of the human health.
Doing the requests to the model it is anticipated to get the information for the setting of diagnosis.
The project has been interrupted in 2016 but the significant contribution in resolving of the problem of symbolic modeling of human health.