Model-Driven Methods to Design of Reliable Multiagent Cyber-Physical Systems? ?? Sergey Staroletov1 , Nikolay Shilov2 , Vladimir Zyubin3 , Tatiana Liakh3 , Andrei Rozov3 , Ivan Konyukhov2 , Innokenty Shilov4 , Thomas Baar5 , Horst Schulte5 1Polzunov Altai State Technical University, Barnaul, Russia 2 Innopolis University, Russia 3 Institute of Automation and Electrometry SB RAS/ Novosibirsk State University, Novosibirsk, Russia 4 Gromov Flight Research Institute (GFRI), Moscow, Russia 5 University of Applied Sciences Berlin (HTW Berlin), School of Engineering Abstract. Cyber-Physical Systems (CPS) are real-world systems that use a cyber part to control a physical part; hybrid systems are virtual-world systems to model CPS. In this paper we address several problems related to CPS-design and argue advantages of a Model-Driven Developing (MDD) approach to CPS-design. We study a simple car stopping system and show that such systems can be modeled without any code writing. However, safety isn’t clear even for this simple system and testing/simulation isn’t sufficient to prove safety, but CPS MDD should be supported by a formal verification also. We examine modeling, simulation and verification tools and show how our approach can be applied. We also introduce a concept of cyber-physical Believe-Desire-Intention (BDI) agent and demonstrate how cooperative agents of this type can predict locations of partners. Keywords: Cyber-Physical Systems · Model-Driven Developing · Believe-Des- ire-Intention agents. 1 Introduction We understand cyber-physical systems (CPS) as real-world systems that use a cyber part (computer/software) to control or operate a physical part (hardware/physical pro- cess). We define hybrid systems as a virtual-world systems that combine continuous real functions with discreet state machines, they are models of the cyber-physical systems. The presence/use of the continuous real functions makes unsuitable techniques which are based on pure discrete state-transition systems and integer arithmetic. Hybrid Systems may be represented by Hybrid Programs, and specified using the Hybrid Dynamic Logic [1, 2]. For example, the syntax of hybrid programs in [3] is ? Partially supported by DFG program Initiation of International Collaboration ?? Copyright c 2019 for this paper by its authors. Use permitted under Creative Commons Li- cense Attribution 4.0 International (CC BY 4.0) defined as follows: α ::= x := e | ?Q | x0 = f (x)&Q | α ∪ α | α; α | α ∗ (1) where α is a meta-variable for the the hybrid programs, x is a meta-variable for program variables, e is a meta-variable for the first-order terms on real numbers, f is a meta- variable for the continuous real functions, and Q is a meta-variable for the first-order formulas over real numbers. The construct ”;” means here the sequential composition, ”∪” — is the non-deterministic choice, ”?” — is the test operator, and ”∗ ” — is the non- deterministic iteration (like Kleene-star). Hybrid Program is a representation of Hybrid Automaton [4]. Modelling and computer implementation of CPSs is not a trivial one-step process, CPSs should be accurately modeled as a hybrid system by teams of physicists, math- ematicians problem-domain (e.g. civil, mechanical, electric, chemical etc.) and control engineers. Fig. 1. Possible problems during implementation of the CPSs Presently there are several ways to implement on computer the physical part of CPSs: – as programs that change the variables according to in-coded exact solutions of the differential equations; the exact solutions can be found analytically or by using symbolic computer algebra tools like Mathematica, Reduce or Maxima; – as programs that numerically solve the differential equations in run-time using, for example, the Runge-Kutta or Euler methods (in simple cases) [5, 6]. The Model-Driven approach (MDD, stands for Model-Driven developing) [7] may be an alternative to the above. It is based on executable diagrams (schemes) for which program code can be generated from them automatically. In the paper, in particular, we address the safety of CPSs created with the MDD approach. Fig. 2. MDD of CPS process with verification of safety properties A possible work-flow of CPSs implementation in the industrial context is shown on Fig. 1. On this diagram we enumerate some problems that may be caused by lose of some details due to change of the abstraction level. The process begins with the creation of mathematical or physical models by en- gineers, who have experience in the specific problem domain and are able to use ap- propriate methods to describe the system in models. As a result, the models have been created, and here we can see possible losses (the model describes the process with some simplifications). Then the model of the process comes to engineer who is in charge for implementa- tion on a device (e.g. controller). The engineer can have misunderstands of the model and therefore, implement the wrong model. Implementing the system, the engineer cre- ates code in one of the programming languages to solve the equations (Physical part) and control features (Cyber part of the CPS). Here the engineer can make mistakes also in the implementation of the mathematical formulas because of the use of floating point formats instead of mathematical real numbers. Also loss of some system behavior, code and model mismatching, etc. can happen in the implementation stage. During a CPS construction, the engineer periodically makes simulations of the created code by run- ning it with some pre-defined test inputs and observing resulting outputs, for example, looking at a plot with the system values evaluation. We note that such simulation is a testing process, it can detect errors and mistakes but not to prove that the implemen- tation is error-free [8]. Moreover, even if the engineer believes that the code acts as correct CPS (because all tests have passed), we need some guaranties whether the code actually represents the CPS initially been expected. As a result of the current process, tested but unproved code goes into a controller (which in addition, has own bugs and limitations) to operate with the real system. 2 Model-Driven Developing of Cyber-Physical Systems MDD is a way to create a software system from scratch by drawing some diagrams or writing textual models and then simulate or execute these diagrams and generate the system code from them. Taking into account the problems discussed in the section 1, we can distinguish the following main advantages of applying MDD in the CPSs design process: – engineers can see a graphical model or a DSL [9] code and move through it; – no code and model distinctions after changing any one of both; – possible ways to generate code for different target languages and purposes (for example, for Matlab Simulink or for implementation in a particular controller); – the system can be created by engineers who know how to describe physical pro- cesses but do not have proper programming skills. So, MDD may be considered as a realistic way to organize work of large teams of engineers to implement CPSs and to improve the quality. Consequently we can update the process shown in Fig. 1, and move to the MDD of CPS design process depicted in Fig.2. According to the process, physicists, mathematicians and engineers work together with a CPS represented by graphical models. They can create symbolic nodes which model different parts of the system and determine relations between them. The engi- neers also detail the requirements expressed in terms of timed logic (see [10] for exam- ple). (Remark, that we are mostly interesting in the safety properties [11], express that ”something (bad) will never happen” during a system execution.) As soon as graphical models and requirements are constructed, it is possible to simulate the system behavior without any code writing. Having safety properties, it is possible to add appropriate assertions (contracts) that may be checked in run-time. Then it may make sense to create on the fly different types of Hybrid Automata which models the Hybrid Program and try different verification tools when needed. And of course, code for a real controller can be generated from the model automatically. 3 Related works 3.1 CPSs modeling languages and tools Certainly, it is possible to implement the Physical part of a CPS by writing code in a pro- gramming language (like C or Java). Dealing with a sophisticated system, it is required to use additional programming libraries to solve different types of ODEs. To realize the Cyber part, network or special hardware libraries should be used. To implement agent- based interoperations, frameworks and languages conform to actor approach [12] can Fig. 3. A survey of CPSs simulation and verification tools be used, for example, Erlang language or Akka library for Java/Scala. Such systems can be organized as multilayer applications with parts implemented in different languages and even act as microservices. A process-oriented technology has been introduced in [13] to express control soft- ware as a set of interacting processes, which are extended automata with special opera- tors that implement concurrent flow control and time-interval managing. This approach has been implemented in a family of languages such as Reflex [13] and IndustrialC [14]. With native support for state machines and floating point operations, these languages allow Hybrid Systems to be easily expressed in code. In the engineering world, currently, a lot of engineers use Matlab Simulink c . It offers to create the CPSs by using a graphical representation very close to the control theory notations. But it lacks of control automata creation in the graphical way, and some portions of the system are still developed by writing lines of code in Matlab language [15]. Another industrial modeling tool is Modelica c [16]. It is a propriatory software that allows to model the dynamic behavior of CPS using different components for mechani- cal, electrical, thermal, hydraulic, pneumatic, fluid, control and other domains. Models can be described by differential, algebraic, and discrete equations. A special model in- put language is used, but there are also graphical editors for it. Ptolemy by Berkeley [17] is a free academic-based tool that supports construction of CPS from small actors at different layers of abstraction. It supports system presen- tation as a multilayer agent that communicate with input/output ports; each agent can represented as a combination of actors and other agents [18]. Actors could be plotting tools, mathematical operations (e.g. differentials), etc. Layers can be automata or state charts, and each layer is controlled by a controller, which can be discrete or continues time unit. The Ptolemy is very extensible, so a developer can implement own actors based on pre-defined interfaces and export the whole system or an actor as Java classes. 3.2 CPSs verification tools Fig. 3 presents some tools for simulation and verification of CPSs. Presented tools may be classified into two categories: 1. tools which provide support both — CPSs modeling and simulation; 2. tools which support only CPSs verification (checking some properties). Uppaal [19] is a model checker and simulator for automata-based programs. User can create a model of a system, including various components in the form of an ex- tended timed automaton and then query some properties (using a variant of LTL for- mulas). User can provide invariants to the model states which can contain timed based derivatives and check them at run-time. Uppaal has some problems with floating point variables and values. Spin [20] is a model checker of programs in an actor-based modeling language Promela (stands for Protocol meta-language) with respect to given LTL formulas. It is a powerful tool to prove the interprocess communications and protocols. It lacks floating point support too; therefore, it cannot be used for full CPSs verification, it can be helpful only to check the Cyber part of the systems with interoperations. SpaceEx tool [21] is distributed as a virtual machine with web-server and includes a model editor, a simulator of CPSs and a converter to PHAVer [22] to verify the proper- ties of such systems over infinite time. It also has model converters from other systems, for example, Simulink, to transform their notation to SpaceEx program. Ariadne [23] can be useful to create non-linear CPSs in C++ code, simulate and verify them. It offers a parametric verification, which provides intervals for values of system variables to preserve the given requirements of the system. Therefore it is pos- sible to use Ariadne with some code checking methods to provide verification of the whole CPS. KeYmaera [24] is an interactive theorem prover based on Dynamic Logic for the CPSs expressed as Hybrid Programs (HPs). The user can prove properties of the system by providing some simplification tactics, or it can be done automatically, that is why the range of systems to be proved in KeYmaera is potentially very wide. The tool can connect to some mathematical systems or solvers at each step of simplification. Please refer our paper [25] for a more detailed survey of these CPSs modeling and verification tools. Please refer also the cited paper for example of verification of a safety property of a simple SPC in C code with Frama-C [26] WP tool which is based on the contracts approach. 4 A case study: MDD approach to car braking system Fig. 4. A top level CPS model and a simulation result Let us consider a car moving with a deceleration according to the following equa- tion:     x0 = v  0 v =a (2)  v20 a = −   2 · (m − x0 ) The negative acceleration a is calculated based on observation at the time t0 (with the speed v0 and initial position x0 ) to a given obstacle m according to a school physical law ”moving with a constant acceleration”. In this section we model the example system with Ptolemy tool to demonstrate how to use the MDD approach to design and simulate such very simple CPS. Fig. 5. The CPS model inside Fig. 6. Braking state refinement In Fig. 4 the top layer model and modeling results are shown. It just plots two model parameters — current position and slowdown of current velocity. In Fig. 5 the model is shown from ”inside” as an automaton with three states – init, braking and stop, where braking – is a Hybrid state that is the subject to further decomposition. In Fig. 6 the braking physical model is actually implemented. It means that the first derivative of the position x is the velocity v, the second derivative of the position is the acceleration a. So, the system model is very close to the real process description, and that simulation doesn’t require any program code writing. 5 Verification problem For the sample system presented in the previous section 4, the safety property could be formulated as ”the car position should be always less the position of the obstacle”. It can be expressed as LTL formula (3): G(x < m) (3) One who looks to the graph in Fig. 4 could say that for the system variables this safety property holds, and the simulation proves it. But as we derived before, the simulation is only a process of quality assurance very similar to testing. For example, the graph can miss sudden function changes due to the small grid size, so for reliable safety systems, we need a mathematically sound way to prove the system properties. That way is the formal model verification process [8]. Fig. 7. Control-flow graph with preconditions, postconditions and invariants [25] as a model of the simple CPS (2) A way to help engineers to start using formal verification — is to integrate the verification process into the tool which is in use for design CPS with MDD approach. In this way, the engineers can apply formal verification without actually getting know how the verification works. As we have mention above in the section 3, Matlab Simulink includes validation instruments. However, these instruments are not of formal verification kind. Currently, the tool is a closed-source and a closed-architecture program, so it is unknown whether it is possible to plug additional model checkers in. The Ptolemy tool has included a model converter [27] to use with some model checkers [28], but now it can convert only discrete time actors. Generation of contin- ues time checking actors, in principle, is possible since the tool is extensible. But the question is: what back-end should be used actually to verify the models? In the paper [25] a graphical way to specify and verify CPSs has been proposed. It can help to prove safety properties by introducing some contracts in control states. For the simple model, a generated control graph is presented in Fig. 7, so after generating proof obligations and HP in KeYmaera theorem prover input language it is possible to prove this system automatically. In mathematical notation, for the system (3) we have the following safe contract for the long-running state braking: (a = −v · v/(2 · (m − x)) ∧ (m > x) → [{x0 = v; v0 = a}](m > x) ∪ (v = 0)). This contract enables proving the safety property automatically without any user inter- action in the theorem prover. 6 Towards Multi-agent Cyber-Physical Systems In this section we proceed to study multi-systems with a number of cyber-physical BDI- agents. A distributed system consists of multiple autonomous individual programmable computers that communicate through a network. Communication (in a distributed sys- tem) is said to be fair, if every computer which needs to communicate with any other will communicate eventually. (Of course, some communication scheduler or mecha- nism is required to guaranty the fairness.) A multi-agent system is a distributed system [29, 30] that consists of agents. A BDI- agent [31] (just agent in the sequel) is an autonomous, reactive and proactive object (in OO-sense) whose internal states may be characterized in terms of Beliefs (B), Desires (D), and Intentions (I). Agent’s beliefs represent its ideas/opinion about itself and the environment that includes other agents and the network; these ideas/opinions may be incorrect, incomplete, and (even) inconsistent. Agent’s desires represent its long-term aims, obligations and purposes (that may be controversial). Agents’ intentions are used for a short-term planning. Agent’s logical omniscience means that an agent immediately knows all logical consequences that follow from its knowledge. We distinguish belief(s) and knowledge according to Plato, that knowledge is a true belief, i.e. a judgment/statement that has a validation [32–34]. Thus we assume in this paper that a belief of some agent becomes its knowledge in some of its individual states if there exists any formal proof of the belief (i.e. we assume agent’s logic omniscience). Reactivity means that an agent can change its beliefs after interaction with other agents and deliberation. Proactivity means that an agent can change its intentions (i.e. to plan its nearest future behavior) after change/update of its beliefs and deliberation. Every agent is autonomous, i.e. a change of its personal beliefs and intentions can’t be decreed by any other agent. A rational agent has clear preferences and al- ways chooses an action (in feasible actions) that leads to the best (individual or group) outcome. A bounded rationality is decision making limited by the cognitive abilities of agents (e.g. the finite amount of time they have to make decisions). A multi-agent algorithm is a distributed algorithm (i.e. protocol of distributed sys- tem) that solves some problem by means of cooperative work of agents in a multi-agent system. A related paradigm is algorithmic mechanism design [35]. Fault-tolerance of a multi-agent algorithm is (as for distributed algorithms) an abil- ity to solve the problem correctly in spite of (partial) network failure and/or incorrect behavior of some of individual agents. A knowledge-based algorithm paradigm [32] as- sumes that any modification of any shared resource may/can be attempted by an agent only when the agent knows that the access for modified resource is safe (i.e. is races-free in particular). Recall that CPS is a system with the Physical (real-world process) part with a con- tinuous behavior (modeled by differential equations) controlled by a programmable computer. A cyber-physical agent is an agent that is CPS itself. A cyber-physical BDI-agent in a cyber-physical multiagent system – knows the differential equation(s) that describes its physical behavior, controls all parameters of this (these) equation(s); – has a belief about equations that model physical behavior of all other agents in the system and ranges of their control parameters. Let us discuss examples of problems to illustrate the difference between just BDI- agents and cyber-physical BDI-agents. Both problem statements have the same start: There are N > 1 autonomous agents (”robots”) and the same number of shelters in general position on a plain part of Mars. Locations of all shelters are fixed and known to all robots. Each robot knows a shelter that was assigned to it from the very beginning, its own distances to all shelters. But then problems differ. The first problem is Mars Robot Puzzle described, solved and (manually) verified in [36] using system of BDI-agents, its statement has the following continuation: Each robot doesn’t know locations of any other robot. All robots can commu- nicate with each other in P2P-manner and every pair of communicating robots may swap their shelters. All robots have to select individual shelters to move in by a straight route. Definitely, robots should not collide (it means that their routes should not intersect). Hence, every individual robot can move to a shel- ter only when it knows for sure that it will not collide with any other robot on the route. Problem: Design a multi-agent knowledge-based algorithm that guarantees that every robot will eventually know that its route to the selected shelter does not intersect with routes of other robots. Let us refer the next problem which we would like to refer Mars-rovers Planning Problem. Its statement has the following continuation: All robot can communicate with each other in P2P-manner and ask/inform each other about their current locations (if requested). All robots have move to the initially assigned individual shelters without approaching each other to close (with individual safety distances). Problem: Design a multi-agent knowledge- based algorithm that guarantees that every robot will eventually reach the as- signed shelter safely (i.e. always being on safe distance with all other robots). This problem can be considered as a special case of the motion-planning [37]. Formal specification and verification (including computer-aided verification) of this problem is one of our topics for further research. In the next section we present first step in this direction — formal specification and (manual) verification of a method how a cyber- physical BDI-agent can predict behaviour of others in a cyber-physical multi-agent sys- tem. 7 Towards predictive cyber-physical agents Agent’s proactivity assumes deliberation i.e. that an agent can “predict” behavior of other agents in a multi-agent system (i.e. it has a belief about behavior of others). Recall also that a BDI-agent in a cyber-physical multi-agent system – knows the differential equation(s) that describes its physical behavior, controls all parameters of this (these) equation(s); – has a belief about equations that model physical behavior of all other agents in the system and ranges of their control parameters. So it implies that an individual belief of a cyber-physical BDI-agent about any particular other agent (a partner) of the system can be represented by a differential equation F(t, y, y0 , . . . , y(n) ) = 0 in which F is a real parameterized expression where – parameters of the expression represent partner’s control features in which the agent believe, – the first argument t is current time, – the second argument y = y(t) is a relative instant location of the partner (with re- spect to the agent itself) at time t, – the third argument y0 = y0 (t) is a relative velocity, i.e. the first derivative of y = y(t), – etc. Let us consider in this section the most simple form for the above equation y0 = f (t, y) where f is a known explicit real expression (i.e. we assume that the agents knows all control features of itself and the partner). Let us discuss how the agent can predict their joint with the partner behavior maintaining some safety condition, i.e. the following prediction problem: the agent – knows the expression for f that describes relative location of the partner and its initial relative location at time tini is yini , – would like to predict the final relative location y f in at time t f in = tini + ∆ and guar- antee that finally they approach each other at distance not less than some known safety radius R > 0. (Remark that we consider here a weak safety requirement while one may be interested in a more strong safety condition stating that the agent and the partner never approach each other at distance less then R.) The problem can be solved, in particular, using the well-known Euler method [6] presented below: – pick-up some n ≥ 1, n ∈ N, such that step h = ∆n is believed to be sufficient for a desired accuracy and let t0 = tini and u0 = yini ; – for each m ∈ [0..(n − 1)], if tm is defined already then let t(m+1) = tm + h, dm = h × f (tm , um ), and u(m+1) = um + dm ; The output consists of a tabular function u that maps each tm (0 ≤ m ≤ n) to um and approximates the exact solution of the equation y0 = f (t, y) in these points in general and the value un approximating y f in in particular. The flowchart of the algorithm that implements a variant of the method to compute just an approximation for the final value y f in is presented in the Fig. 8. Fig. 8. The flowchart of an Euler Algorithm that computes an approximation for the final value using Euler method A quite common variant of applicability (sufficient) conditions for the Euler method [6] comprises the following three properties: 1. ∆ > 0 and n > 0 are positive real and integer numbers, tini ∈ R and t f in = tini + ∆ are reals; 2. f : [tini ,t f in ] × R → R is uniformly Lipschitz continuous in the second argument (formally defined below); 3. there exists a twice continuously differentiable solution y : [tini ,t f in ] → R of the initial value problem y0 = f (x, y), y(tini ) = yini . Recall that a function g : R → R is Lipschitz continuous, if there exists a real con- stant q > 0 such that |g(x + δ ) − g(x)| ≤ q · δ for all x ∈ R and positive δ ∈ R+ . In particular, Lipschitz continuity in the second argument for a function f : [tini ,t f in ] × R → R means that for every t ∈ [tini ,t f in ] there exists a real constant q > 0 such that | f (t, x + δ ) − f (t, x)| ≤ q · δ for all x ∈ R and positive δ ∈ R+ . In contrast the above condition 2 about an uniform Lipschitz continuity in the second argument for func- tion f : [tini ,t f in ] × R → R means that there exists a real constant q > 0 such that | f (t, x + δ ) − f (t, x)| ≤ q · δ for all for t ∈ [tini ,t f in ], x ∈ R, and positive δ ∈ R+ ; let us refer the constant q in this case as Lipschitz constant for f in the second argument. Let a, b ∈ R, a ≤ b and n ∈ N be real and natural numbers. A function g : [a, b] → R is n-times continuously differentiable (notation g ∈ C(n) [a, b]), if the function has derivatives g(0) ≡ g : [a, b] → R, ... g(n) : [a, b] → R, and all these functions are con- tinuous on [a, b]: g(0) , . . . g(n) ∈ C[a, b]. In particular the above condition 3 says that g ∈ C(2) [tini ,t f in ], i.e. that y, y0 , and y00 are defined and continuous at each point of [tini ,t f in ]. Recall the extreme value theorem (also known as Weierstrass theorem) states that if a real-valued function g is continuous on the closed interval [a, b], then g must attain its maximum and minimum (least once each); hence the condition 3 implies that there exists a real constant p > 0 that is an amplitude for |y00 | (i.e. such that |y00 | ≤ p for all t ∈ [tini ,t f in ]). Thus the above variant of applicability conditions for the Euler method for a pre- dictive cyber-physical BDI-agent can be reformulated as follows: 1. ∆ > 0 is a time-interval after which the agent would like to know a relative loca- tion of the partner, n > 0 is a positive integer number that the agent believes to be sufficient for partitioning the time-interval ∆ , tini and t f in = tini + ∆ are the initial and the final time readings known for the agent; 2. f : [tini ,t f in ] × R → R is a known for the agent law that returns partner’s relative speed (as a function of time and relative location) and that the agents knows that the function is uniformly Lipschitz continuous in the second argument with Lipschitz constant q > 0; 3. the agent knows the initial relative location of the partner yini at time tini and that the relative acceleration of the partner is a continuous function on [tini ,t f in ] with some constant amplitude p > 0. Let us denote all these three conditions altogether as Initial Knowledge. The above variant of applicability conditions for the Euler method [6] guarantees that upon termination of the method for all m ∈ [0..n] p  q(tm −tini )  |y(tm ) − um | ≤ e −1 h 2q where q is the Lipschitz constant for f in the second argument and p > 0 is an amplitude of y00 on [tini ,t f in ]. Since we are interested in the prediction of the final relative location exclusively then this property transforms into the following Guarantied Location con- dition: p ∆   |y(t f in ) − y f in | ≤ × × eq∆ − 1 . 2q n Fig. 9. Control-flow graph with preconditions, postconditions and invariants as a model of the predictive cyber-physical BDI agent Conditions Initial Knowledge and Guaranteed Location altogether with the Euler- Algorithm give us the following total correctness assertion [38] [Initial Knowledge] Euler Algorithm [Guaranteed Location] that states that if the agent has the Initial Knowledge then the Euler Algorithm terminates and the Guaranteed Location holds upon termination. If one would like to prove the assertion formally then – the precondition Initial Knowledge should be assigned to the control point 1, the postcondition Guaranteed Location should be assigned to the control point 3 in the flowchart in Fig. 8, – the invariant consisting of the following two properties • 0 ≤ m ≤ n and t  = tini + h · m,  k • |y(t) − u| ≤ 2p × ∑k=m−1 k=0 (1 + q · h) × h2 should be assigned to the control point 3 in the flowchart in Fig. 8. The proved total correctness assertion gives us an opportunity to provide an estima- tion for n that guaranties the weak safety condition. Really, since p ∆   |y f in | − |y(t f in )| ≤ |y f in − y(t f in )| ≤ × × eq∆ − 1 2q n then p ∆   |y f in | − × × eq∆ − 1 ≤ |y(t f in |; 2q n   p so R < |y(t f in )| if R + 2q × ∆n × eq∆ − 1 < |y f in |, i.e. in the case when p ∆   |y f in | > R and n > × × eq∆ − 1 . 2q |y f in | − R 8 The control-based verification of cyber-physical agents In the previous section 7, we stated that the predictive cyber-physical BDI-agent prob- lem can be reduced to contract verification. In the mathematical way, with the variables introduced before, staying in a long-running state could be described as ∆ (∆ > 0) ∧ (n > 0) ∧ (h = ) ∧ (m = 0) ∧ (t = tstr ) n ∧(u = ystr ) → [d = h · f (t, u); u = u + d;t = t + h; m = m + 1] p ∆   (y f in = u) ∧ |y(t f in ) − y f in | ≤ × × eq∆ − 1 . 2q n . So, the control graph method and verification in KeYMaera with the provided con- tract are applicable here, and that graph is shown in Fig. 9. This system can be proved with KeYmaera prover without user interaction after generating the HP code from the control-flow graph or by using any contract based prover after one will write a code of system for Euler method described in Fig. 8 and provide precondition, postcondition and invariant described in this section. Nevertheless, for the more general problem of robots communicating, when each robot has this own function and needs to predict others robots moving, system specifi- cation will become not a simple task and verification of this definitely require automatic HP code generation by the model and developing of the system should be model-based. When robots start to use P2P communication, engineers should also use the Cyber part verification methods to prove the protocol, it is possible to use the methods described in the References section of this paper, and in future it is better to have all the methods integrated into the one tool. 9 Conclusion In this paper firstly we addressed the problem of Cyber-Physical Systems (CPSs) mod- eling and validation. We state that Model-Driven Development (MDD) approach should be applied and there are some tools which support construction the CPSs with various level of abstractions without any code writing. Next we discussed CPSs verification problem, and state that for a robust system design we need to use formal verification methods and tools. Because the CPSs need the Dynamic Logic to model the equations over the continuous time, it is hard to verify such systems with conventional verification tools designed for discrete-state systems. We state that right now there is a deficit of industrial-strong tools which provides veri- fication of both the Cyber and the Physical parts of a CPSs. Then we considered a sample CPS — a car braking example to show how to model and verify CPSs easier. Finally we moved to the conception of cyber-physical BDI agents to show various problems with it. The Mars Rovers problem for robot-of-robot prediction can be nu- merically solved with using the Euler method, and this method helps to construct the considered verification strategy for this problem using our control-flow graph approach. But for the problems that require BDI agents interoperations (for example, in a P2P manner) it is hard to describe and model the system behavior and provide the verification strategy. We think that a Model-Driven method to design and verify such types of systems should be developed. The topic for the further research is to extend the control-flow graph approach to convert the existing engineering notations to an intermediate representation and then automatically create Hybrid Automata, proof obligation and verify them with the KeY- maera theorem prover or other suitable methods. References 1. A. Platzer, “Differential dynamic logic for verifying parametric hybrid systems.” in TABLEAUX, ser. LNCS, N. Olivetti, Ed., vol. 4548. Springer, 2007, pp. 216–232. 2. Platzer, André, “Differential dynamic logic for hybrid systems,” Journal of Automated Rea- soning, vol. 41, no. 2, pp. 143–189, 2008. 3. A. Platzer, “Logical Foundations of Cyber-Physical Systems,” Switzerland: Springer, 2018. 4. T. A. Henzinger, “The theory of hybrid automata,” in Verification of Digital and Hybrid Systems. Springer, 2000, pp. 265–292. 5. E. Hairer, C. Lubich, and M. Roche, The numerical solution of differential-algebraic systems by Runge-Kutta methods. Springer, 2006, vol. 1409. 6. W. Trench, Elementary Differential Equations. Thomson Learning, 2001. [Online]. Available: https://digitalcommons.trinity.edu/mono/8/ 7. B. Selic, “The pragmatics of model-driven development,” IEEE software, vol. 20, no. 5, pp. 19–25, 2003. 8. S. Staroletov, Basics of Software Testing and Verification [in Russian]. Lanbook, Saint Petersburg. ISBN 978-5-8114-3041-3, 2018. 9. L. Bettini, Implementing domain-specific languages with Xtext and Xtend. Packt Publishing Ltd, 2016. 10. D. Lozhkina and S. Staroletov, “An online tool for requirements engineering, modeling and verification of distributed software based on the MDD approach,” Some Journal, 2008. 11. E. Kindler, “Safety and liveness properties: A survey,” Bulletin of the European Association for Theoretical Computer Science, vol. 53, no. 268-272, p. 30, 1994. 12. G. A. Agha, “Actors: A model of concurrent computation in distributed systems.” Mas- sachusetts Inst Of Tech Cambridge Artificial Intelligence Lab, Tech. Rep., 1985. 13. V. E. Zyubin, “Hyper-automaton: A Model of Control Algorithms,” in IEEE International Siberian Conference on Control and Communications (SIBCON-2007). Proceedings., O. Stukach, Ed. Tomsk, Russia: IEEE, 2007, pp. 51–57. [Online]. Available: https://doi.org/10.1109/SIBCON.2007.371297 14. A. S. Rozov and V. E. Zyubin, “A hyperprocess-based approach in Arduino programming,” International Conference on Advanced Technology & Sciences (ICAT’15), 2015. 15. H. Moore, MATLAB for Engineers. Pearson, 2017. 16. P. Fritzson, Principles of object-oriented modeling and simulation with Modelica 2.1. John Wiley & Sons, 2010. 17. J. Davis II, M. Goel, C. Hylands, B. Kienhuis, E. A. Lee, J. Liu, X. Liu, L. Muliadi, S. Neuendorffer, J. Reekie et al., “Overview of the Ptolemy project,” ERL Technical Re- port UCB/ERL, Tech. Rep., 1999. 18. S. Staroletov, “Towards problems of cyber-physical systems verification while designing them with the model-driven approach,” 16th International Scientific-Practical Conference of Students, Post-graduates and Young Scientists “Youth and Modern Information Technol- ogy” (YMIT), 2018. 19. A. David, K. G. Larsen, A. Legay, M. Mikučionis, and D. B. Poulsen, “Uppaal smc tutorial,” International Journal on Software Tools for Technology Transfer, vol. 17, no. 4, pp. 397–415, 2015. 20. G. J. Holzmann, “The model checker SPIN,” IEEE Transactions on software engineering, vol. 23, no. 5, pp. 279–295, 1997. 21. G. Frehse, C. Le Guernic, A. Donzé, S. Cotton, R. Ray, O. Lebeltel, R. Ripado, A. Girard, T. Dang, and O. Maler, “SpaceEx: Scalable verification of hybrid systems,” in International Conference on Computer Aided Verification. Springer, 2011, pp. 379–395. 22. G. Frehse, “Phaver: algorithmic verification of hybrid systems past hytech,” International Journal on Software Tools for Technology Transfer, vol. 10, no. 3, pp. 263–279, 2008. 23. L. Benvenuti, D. Bresolin, P. Collins, A. Ferrari, L. Geretti, and T. Villa, “Ariadne: Domi- nance checking of nonlinear hybrid automata using reachability analysis,” in International Workshop on Reachability Problems. Springer, 2012, pp. 79–91. 24. A. Platzer and J.-D. Quesel, “KeYmaera: A hybrid theorem prover for hybrid systems (sys- tem description),” in International Joint Conference on Automated Reasoning. Springer, 2008, pp. 171–178. 25. T. Baar and S. M. Staroletov, “A control flow graph based approach to make the verification of cyber-physical systems using KeYmaera easier,” Modeling and Analysis of Information Systems, vol. 25, no. 5, pp. 465–480, 2018. 26. F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles, and B. Yakobowski, “Frama-c: A soft- ware analysis perspective,” Formal Aspects of Computing, vol. 27, no. 3, pp. 573–609, 2015. 27. C.-H. Cheng, T. Fristoe, and E. A. Lee, “Applied verification: The Ptolemy approach,” Some Journal, 2008. 28. E. M. Clarke Jr, O. Grumberg, D. Kroening, and H. Veith, Model checking. Cyber-Physical Systems, 2018. 29. M. Takada, “Distributed systems: for fun and profit,” 2013. [Online]. Available: http://book.mixu.net/distsys/ 30. A. Tanenbaum and M. van Steen, Distributed Systems: Principles and Paradigms, 2nd ed. Prentice-Hall, 2006. 31. M. Wooldridge, An Introduction to Multiagent Systems, 2nd ed. John Willey & Sons, 2009. 32. R. F. R., J. Halpern, Y. Moses, and M. Vardi, Reasoning about Knowledge. MIT Press, 1995. 33. J. Ichikawa and M. Steup, “The analysis of knowledge.” [Online]. Available: http://plato.stanford.edu/entries/plato-theaetetus/ 34. C. Chappell, “Plato on knowledge in the theaetetus.” [Online]. Available: http://plato.stanford.edu/entries/plato-theaetetus/ 35. P. Dütting and A. Geiger, 2007. [Online]. Available: http://www.staff.science.uu.nl/l̃eeuw112/msagi/mech design.pdf 36. N. Shilov, N. Garanina, and E. Bodin, “Multiagent approach to a dijks-tra problem,” in CS&P’2010 Workshop on Concurrency, Specification and Programming. Humboldt- Universitat zu Berlin, 2010. 37. S. LaValle, Planning Algorithms. Cambridge University Press, 2006. 38. Z. Manna and A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems: Specifi- cation, 2nd ed. Springer, 2012.