In the article the platform for modeling of algebraic behavior is considered. It is intent for formalization of the systems, especially distributed, their modelling and analysis of the properties. Platform is used for the formal verification, model-based testing and security issues detection. Behavior algebra specifications are used as the modeling language. The number of projects is considered in the paper implemented on platform in cybersecurity, blockchain solutions and legal requirements processing.
The current stage of development of the software systems industry is characterized by a significant complication of the process of their development. Today are widely used cyber-physical systems, blockchain technologies, and, in particular, smart contracts, Distributed ledger technology (DLT), etc.
Cyber-Physical Systems (CPS) are used in space research, transport management,
in the energy sector, in production management, in the military sphere, in medicine, in
the construction of modern infrastructure, for contactless control of consumer
electronics, etc. Typically, CPS are the systems with critical application area. Therefore,
when designing such systems, increased demands are placed on their reliability and
safety [
Distributed ledger technology is information storage technology, the key features
of which are the sharing and synchronization of digital data according to the
consensus algorithm, the geographical distribution of equivalent copies at different points
around the world, the absence of a central administrator [
Transaction denial attacks, Desynchronization attacks, 51% attacks, Selfish-mining, etc.
At the same time, the existing methods of quality control of the developed systems are characterized by incompleteness, high complexity and insufficient reliability. This situation inevitably entails an increase in the number of errors in the development of systems.
As a rule, an analysis of the compliance of a system with the requirements that are imposed on it is carried out either by means of its visual analysis or by a testing method. However, if any of the properties of the system can be formally expressed, for example, in the form of a formula of mathematical logic, then the analysis of this property can be carried out by verification methods.
As a rule, verification is used to analyze the first requirement to the system - its correctness. Note, that this requirement is the main one.
In the first section of this article, a brief description of the current state of theoretical studies in the field of verification and short overview of developed systems for model verification is given. In second section of this article our approach to verification and model testing is presented. The third section of this article describes the Main capabilities and functionality of the platform. In the fourth section a short description of few examples of implemented models is given. 2
The problems of modeling and verification of software systems occupy a central position in research on the mathematical theory of programming. This is primarily due to the high relevance of creating a theoretical foundation for the development of reliable software.
In [
Since 1970, more than 25 research projects on the use of information technology in
legal activity have been developed. The problem of using information technology to
legal regulation is not new to the EU, so there are legal policy modeling systems in
the EU: EUROMOD, SYSIFF and POLIMOD. In Finland and the Netherlands,
JURIX was created by the organization of researchers in the field of law and
informatics, who are engaged in computer analysis of legal texts and documents. Thus,
article [
In [
Over the past five years found a place the Semantic Web technology and using of
ontologies theory in jurisprudence. Thus, tools based on the Semantic Web and
ontology theory are generally intended not only to optimize the search for legal
information, but also as a tool for clustering, classifying and managing legal
knowledge [
The paper [
The article [
There are various technologies of requirements verification. You can use the traditional method of model checking (model checking) or use deductive methods of symbolic modeling (symbolic modeling) with using an automatic proofing and specialized programs such as provers and solvers.
There are many of tools for simulation modeling of behavior in different domains, such as Maple, MatLab, Powersim, Ithink, Arena for economic modeling, SmartCheck, EtherTrust, ZEUS for smart-contracts, EUROMOD, SYSIFF and POLIMOD for jurisprudence, etc.
All systems are popular and can be used in various scientific fields. But the rapid pace of information technology development, and, in turn, the increasing complexity of software, requires to finding new approaches and solutions. That is why we are working to improve formalization technologies. We use algebraic methods to solve problems more precisely and use more expressive languages.
The study is a continuation of the previous authors works in which were presented using methods of algebraic programming and insertion modeling for verification and simulation of crypto-economics, legal, economics models, hardware systems.
At the articles [
In the paper [
An example of describing CPS in the IMS system is presented in [
In the papers [
Model verification is to investigate the behavioral properties of safety or viability. To prove the reachability of the properties, that are checked, can be used the following formal methods of behavior algebra: • Static - methods for which it is sufficient to prove the feasibility property that is given by the formula in the base language. In other words, there are some values of formula attributes where the formula can be true. Proof of the property of feasibility is achieved by the using of solving machines such as Microsoft Z3 and cvc4. • Dynamic - Applied to behavioral properties (properties where the formula is represented by expressions of behavior algebra and by semantics of actions, where the formula is represented as an expression in the base language) [21]. • Combined - methods for which the proving of feasibility of formulas is not enough, and it is necessary to prove the reachability of the formula by symbolic modeling. • Partially dynamic - use the technique of invariants generating [22] in behavior algebra.
A model in the form of algebra of behavior and the property formula, that is verified, are inputs to the verification procedure, and verdict that confirms its reach and a scenario that leading to the corresponding state is its output.
Within the framework of behavior algebra uses such basic verification methods as incompatibility (nondeterminism), incompleteness (deadlocks), compatibility of timing properties, and synchronization problems, critical states (expressing a state of "starvation" when all agents are waiting for receiving of signals, a state of violation of restrictions or other security properties that can be specified by the user), signals racing (when different signal sequences create different states of the environment), properties of liveness, that expressing the reachability of the desired state.
Model testing. To create a test set in a suitable testing environment, an algebraic model can serve as a model for traces generating. At each of the development phases can be checked model artifacts. Both design specifications and binary code can be tested. Direct and inverse symbol modeling are the main methods of test generation.
Necessary covering of code lines by tests is determined by both the requirements for the generation of tests and the model where exhaustive testing can be considered, namely, the generation of all possible states of model behavior, coverage of actions in a model, or coverage of all transitions between actions.
The test is the sequence of reception and sending signals between agents. When performing tests, there are two instances - instance that tests and instance that being tested. Test signals are sent to tests instance and then performed a comparison with the expected result.
The following types of testing are considered when using behavior algebra: • black box method - a set of tests where the code of the instance that being tested is unknown; • white box method. The process is determined by the symbolic execution of the parallel composition of model and code. When execution, the states of the environment are compared on equivalence. 4 4.1
APS was developed by the Glushkov Institute of Cybernetics of the National Academy of Science of Ukraine. It was the first system of term rewriting which used the systems of rewriting rules and rewriting strategies separately [23]. The main goal of APS is to create an algebraic program that solves mathematical problems. APS include Proving and Solving Systems.
A Proving System give us a possibilities to prove some trueness of a formula in a theory if the axioms and relation are given. For the resolving equations in Solving Systems in APS are implemented the fol-lowing theories: enumerated types theory, Boolean logic, linear arithmetic, float arithmetic, string solving, and etc.
Insertion modeling focuses on building of models and studying the interaction of agents and environments in complex distributed multi-agent systems. The main notion of IMS is the insertion function, which defines the behaviors of agents and actions of environments. We used the behavior algebra specifications for the formalization for the insertion modeling method [25] and the deductive or symbolic method in IMS based on the such external provers and solvers, as Presburger – omega, FourierMotzkin - reallib (our tool), cvc3, z3 and MathSAT.
An Algebraic Engine is an algebraic tool for modeling of system behavior. It is created on the basis of the IMS system.
It has the following features: • Generation of symbolic behavior scenarios; • Resolve the problem of reachability of some property (safety, liveness, and security violations). It detects the reachability of a property given as a formula and given as a behavior in a behavioral algebraic expression; • Provide verification by symbolic modeling (with the usage of slice technique) of protocols, programs, models and other behavioral specifications given in behavioral algebraic expressions; • Map symbolic modeling to original language specifications.
The main features of SymTech Platform are: • testing technologies; • model-driven development; • support of the development process of a critical system or system with Quality of
Service (QoS); • verification and validation; • cybersecurity. 4.2
SymTech (Symbolic Modeling) platform includes a number of system and libraries for implementation of the algebraic formal methods and integration with other program systems.
To get started, you must log in to your account on the platform. Once you have logged into your account, you can create a new project, or open a previously created one. After creating a new project, you will see the following arrangement of menus and windows (Fig. 1):
Thus, we have a vertical and horizontal menu for our platform: • Horizontal menu. Gives us possibilities to make some manipulations with project, such as: back to previous and next action; create, save, start, copy, export or import of project; creation of different experiment with a model, creation a copy of experiment. • Vertical menu. In this menu we see the list of items that are the key definitions of formalization and are the basis for model formalization and, also a list of special platform tools.
As you can see, the main workspace is occupied by such windows as "protocol", "behavior", "console", etc. (Fig.1). They open by default, but can be closed, minimized or maximized depending on your needs. In these windows, after creation, will be displayed the key elements of the model, startup results (in console), etc. We also will use them to edit and describe the necessary elements. Let's consider the main functionality of the platform on the concrete examples. 4.3
In this example we describe the model of how a coffee machine works.
We have an automated machine which interacts with the external environment by means of coins - input data, of certain denomination and two buttons - «Make coffee» and «Cancel». Requirements for the operation of a coffee machine are given below.
Requirements for the operation of a coffee machine. • R1. The coffee machine contains slots for 5, 10, 25, 50 cent coins, display and sensor buttons «Make coffee» and "Cancel". • R2. The coffee costs 95 cents. • R3. After inserting coins into the slot corresponding to the amount, the sum will be shown on the display. • R4. If the total of inserted coins is greater or equal to 95 cents, then after pressing the button «make coffee» a drink is delivered and the corresponding change returned. • R5. Upon pressing the button "Cancel," after inserting coins, the total amount will be refunded.
The example contains agent – automatic machine which interact with the external environment.
Requirement R1 states that the agent - automatic machine communicates with the environment by means of coins - input data, of certain denomination and two buttons, which can be written as the following, having entered the appropriate integer attribute coin, satisfying the condition:
(coin = 5)|/ (coin = 10)|/ (coin = 25)|/ (coin = 50) Requirement R2 says that there is a certain factor that contains attributes of price, which can be written down as the following:
CoffeePrice = 95 The requirements enclose one more attribute related to the amount of inserted coins. Let’s designate it by means of the identifier “SUMMA.”
It is also required to define the obvious fact that if no coins were inserted into the automatic machine, then SUMMA = 0. Thus the agent is formed with variety of attributes which form its type.
For creating a model at the platform we must make next steps:
tributes. In the vertical menu yuo can see item "Agent types" (Fig.2 (a)) in that we can add types of agents. After that we can choose needed agent type and in the special window we can add agent attributes (FIg.2 (b)). 2. Add an Agents. After the finishing of the describing of all agents types, we must add the instances of agents. In our example, it's only one agent. The agent name is CoffeeMach1 and its type is CoffeMachine (Fig.3(b)).
It is important to identify the type of agent in those cases when there are only a few of them and the agent expressions shall be used for making these distinctions. In this simple given example, so long as there is only one agent we can consider agent attributes as attributes of the environment. 3. Add Trigger Events. The next step is to determine all trigger events (Fig.4). Requirements R3, R4, R5 describe the reaction of the agent to exposure in the environment. They explicitly define trigger events – insert coins, press button “make drink,” push button, “return of the sum.” Thus, preconditions for triggers - presence of inserted amount and the fact that the inserted sum is greater or equal to the price of coffee - are explicitly defined.
Such as one of the trigger events is "insert coins," so we declare, for this event, the parameter x of integer type. 4. Add Basic Protocols. All basic protocols are presented in the list of "Basic protocols" in the vertical menu. Any of them must be described on the special tab "Basic protocols". Their MSC-diagrams must be described on this tab too (Fig.5). It should be mentioned, that the attribute coin was not defined at first. The attribute coin in Insert_Coins protocol is used as a parameter of basic protocol or local attribute whose value is saved only during the execution of basic protocol. After the application of a basic protocol, it becomes indefinite again. 5. Initial Environment. In the Initial Environment we describe the initial values (Fig.6) 6. Behavior. Requirements do not clearly define a certain sequence of application of basic protocols. Initially, only the R3 protocol can be applied and the rest after including itself. After the R4 protocol it is possible to repeat preparation of new portion of drink or complete operation. This sequence is represented in the form of the following UCM-diagram (Fig.7)
The reflection of UCM-notation in a text form must be written in the tab "TEXT." For this example, we have the following description (Fig.8). 7. Simulation results. After starting the program of trace symbolic generation, we get a result, where the behavior of the model is represented by eighteen traces (Fig.9). The text verdict which contains the statistics of trace generation is created after the end of the operation of trace generation. The number of traces, which leads to the state determined by goal, state the formula such as deadlock states, visited states, states of safety violation and states of possible non determinism is displayed.
The statistics of basic protocol application and the list of not applied basic protocols are provided. The time of trace generation is also documented.
In the given traces information display regarding the symbolic state of the environment, is disabled and there are only those elements illustrating the application of basic protocols, namely messages in the form of arrows and the local actions of an agent. 5 5.1
SKILLONOMY is an educational online platform that tokenizes productive activities in the learning process and is focused on gaining monetized online knowledge and skills. The SKILLONOMY ecosystem is built around an IT platform that allows participants to effectively build and administer the relationships that are related to training, investing and sharing experience. Developing the SKILLONOMY project required a set of essential functions of the blockchain for ensuring a stable and efficient system that works [26].
The main purposes of the tokenomics model formalization of the SKILLONOMY project are: • the search for modeling errors, such as finding failings or possible contradictions; • the search for effective scenarios of the system in the model, etc.; • the possibilities for analyzing and predicting the model; and • the possibilities for analyzing the feasibility of project financing.
The process of the formalization of the tokenomic project consists of the following steps: selection of the agents and definition of their attributes corresponding to the level of abstraction demanded, definition of agents’ actions and the design of agents’ behavior.
As a result of the simulation of the model and with the selection of different values of attributes, we were able to analyze the behavior of the SKILLONOMY model according to different bitcoin trends.
When we model the specifications, we simulated the activity of all agents that take part in such processes as sending and receiving tokens and selling and purchasing tokens on the stock exchange. In the process of modeling, we were able to monitor the dynamics of attributes and main tokenomic indicators. Moreover, unlike to previous results, in the latest version of model we have modeling the situation when in the system can be present two or more students group and the number of students may increase.
This model allows changing hypotheses to evaluate the risks when selecting the worst conditions in the process of tokenomic modeling. One of most important advantages of tokenomic modeling is the opportunities to debug the system and to change the algorithm or boundary values of attributes to reach the demanded results.
Description of the model is given in [
The algebraic approach in cybersecurity was demanded over the past two decades with the appearance of efficient solving and deductive tools. Different techniques like symbolic modeling and concolic computations use the algebraic approach that has created more possibilities for methods of detection in cybersecurity.
Our tools anticipate algebraic matching in different modes. The following applications are available and are under active research: 1. Definition of Attacker Behavior
The project has been started together with the Glushkov Institue of Cybernetic in 2017. The goal of the project is to use the algebraic formal methods in the detection of attack and vulnerability in the software systems.
One of the decisions is the usage of behavior algebra algorithms and the theory of insertion modeling. Types of intruder attacks from CVE database, especially Meltdown and Spectre are presented as behavior algebra expression and detection of vulnerability is defined by resolving of behavior. 2. Vulnerabilities Detection
The project has started 2016 year with the attempts to formalize the vulnerability “Heartbleed” and try to detect it in Algebraic Programming System.
The results (together with V.Sukhomlinov from Intel) are presented in a paper [27].
The technology of vulnerability formalization has been developed together with the Institute of cybernetics. The technique of vulnerability semantics presentation in behavior algebra expressions has been presented in papers [28, 29]:
The main benefit of an algebraic approach is that we can more accurately detect vulnerabilities. The description of the vulnerability covers a set of its possible scenarios.
The implementation of two or more matching levels can significantly increase the detection efficiency. Thus, matching at the control flow level can be implemented first as a fast procedure, and then, the detected set of scenarios can be modelled symbolically as the more expensive stage. 5.3
We considered the subset of Tax Code and created it’s formalization that contains all articles belonged to VAT (Value Added Tax) and its dependencies from additional by-laws.
For presentation of algebraic model we use double sort algebra that contains the algebra of behavior and logical language with arithmetic, set-theoretic and logic operations. Formulas of this language are constructed from operations and predicates over integer, real, enumerated, and symbolic types [30].
Usually in Tax Code we have two kinds of agents that are – tax payer and taxation office. We can consider the set of Tax Payers that interact with each other.
The given approach could be applied to legal requirements that could be formalized by such manner. We can watch the possible scenarios and analyze the environment in system to achieve the right formal presentation. The traces were verified by third person with economic background and corresponding correction were made.
Now the “digital” Tax Code of Ukraine is ready for use in the scope of Algebraic Programming System and could be deployed in interested organization.
Description of the model is given in [
Behavior algebra and basic protocol specifications are used for the formal description of a model. Algebraic artifacts such as theorems and abstract algorithms provide a basis for formal verification methods. These methods were implemented and successfully applied to industry projects in Motorola, Inc.
Formal verification anticipates the checking of the properties of the system. The properties could be classic, such as the absence of deadlocks and non-determinisms, or subject domain specific defined safety or liveness conditions. We can prove the reachability of demanded properties by using a symbolic modeling method developed in the scope of IMS.
The given approach could be applied to models that could be formalized by such manner. One of the difficulties is the process of formalization. Due to the experience there should be two specialists involved in the process of the formalization – algebrists and specialist in specific area of project.
We would like to thank the company LitSoft Enterprise R&D [31] for the opportunity to work with the platform for modeling of algebraic behavior for our research and experiments in the modeling area. We are also grateful to the Glushkov Institute of Cybernetics of NAS of Ukraine for the theoretical and practical results in the field of verification that were used as a basis for our studies of formalization and algebraic modeling in the tokenomics projects area and to the Kherson State University for the active supporting of Insertion Modeling System.