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.
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 process). 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 [
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,
mathematicians problem-domain (e.g. civil, mechanical, electric, chemical etc.) and control
engineers.
– 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) [
The Model-Driven approach (MDD, stands for Model-Driven developing) [
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 engineers, who have experience in the specific problem domain and are able to use appropriate 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
implementation 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
creates 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
running 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
implementation is error-free [
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
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 [
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
engineers also detail the requirements expressed in terms of timed logic (see [
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 3.1
Certainly, it is possible to implement the Physical part of a CPS by writing code in a
programming 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
agentbased interoperations, frameworks and languages conform to actor approach [
A process-oriented technology has been introduced in [
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 [
Another industrial modeling tool is Modelica c [
Ptolemy by Berkeley [
1. tools which provide support both — CPSs modeling and simulation; 2. tools which support only CPSs verification (checking some properties).
Uppaal [
Spin [
SpaceEx tool [
Ariadne [
KeYmaera [
Please refer our paper [
Let us consider a car moving with a deceleration according to the following equation: 8>x0 = v > ><v0 = a >>>a = :
v20 2 (m x0) (2) 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. 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 [
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 [
In the paper [
x)) ^ (m > x) ! [fx0 = v; v0 = ag](m > x) [ (v = 0)): This contract enables proving the safety property automatically without any user interaction in the theorem prover. 6
In this section we proceed to study multi-systems with a number of cyber-physical BDIagents.
A distributed system consists of multiple autonomous individual programmable computers that communicate through a network. Communication (in a distributed system) is said to be fair, if every computer which needs to communicate with any other will communicate eventually. (Of course, some communication scheduler or mechanism is required to guaranty the fairness.)
A multi-agent system is a distributed system [
We distinguish belief(s) and knowledge according to Plato, that knowledge is a true
belief, i.e. a judgment/statement that has a validation [
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 always 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
system) that solves some problem by means of cooperative work of agents in a multi-agent
system. A related paradigm is algorithmic mechanism design [
Fault-tolerance of a multi-agent algorithm is (as for distributed algorithms) an
ability 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 [
Recall that CPS is a system with the Physical (real-world process) part with a continuous 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
Let us discuss examples of problems to illustrate the difference between just BDIagents 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 [
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
knowledgebased algorithm that guarantees that every robot will eventually reach the
assigned 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 [
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
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 respect 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 + D and guarantee 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 [
A quite common variant of applicability (sufficient) conditions for the Euler method
[
Recall that a function g : R ! R is Lipschitz continuous, if there exists a real constant q > 0 such that jg(x + d ) g(x)j q d for all x 2 R and positive d 2 R+. In particular, Lipschitz continuity in the second argument for a function f : [tini; t f in] R ! R means that for every t 2 [tini; t f in] there exists a real constant q > 0 such that j f (t; x + d ) f (t; x)j q d for all x 2 R and positive d 2 R+. In contrast the above condition 2 about an uniform Lipschitz continuity in the second argument for function f : [tini; t f in] R ! R means that there exists a real constant q > 0 such that j f (t; x + d ) f (t; x)j q d for all for t 2 [tini; t f in], x 2 R, and positive d 2 R+; let us refer the constant q in this case as Lipschitz constant for f in the second argument.
Let a; b 2 R, a b and n 2 N be real and natural numbers. A function g : [a; b] ! R is n-times continuously differentiable (notation g 2 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 continuous on [a; b]: g(0); : : : g(n) 2 C[a; b]. In particular the above condition 3 says that g 2 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 jy00j (i.e. such that jy00j p for all t 2 [tini; t f in]).
Thus the above variant of applicability conditions for the Euler method for a predictive cyber-physical BDI-agent can be reformulated as follows: 1. D > 0 is a time-interval after which the agent would like to know a relative location of the partner, n > 0 is a positive integer number that the agent believes to be sufficient for partitioning the time-interval D , tini and t f in = tini + D 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 [
[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, jy(t) uj 2p åkk==0m 1 (1 + q h)k 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 estimation for n that guaranties the weak safety condition. Really, since jy f inj jy(t f in)j jy f in y(t f in)j p 2q
D n eqD 1 then so R < jy(t f in)j if R + 2pq eqD eqD jy f inj > R and n > eqD
In the previous section 7, we stated that the predictive cyber-physical BDI-agent problem 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 D n (D > 0) ^ (n > 0) ^ (h =
) ^ (m = 0) ^ (t = tstr) ^(u = ystr) ! [d = h f (t; u); u = u + d; t = t + h; m = m + 1] (y f in = u) ^ jy(t f in) y f inj p 2q
D n eqD 1 : .
So, the control graph method and verification in KeYMaera with the provided contract 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 specification 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
In this paper firstly we addressed the problem of Cyber-Physical Systems (CPSs) modeling 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 verification 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 numerically 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 KeYmaera theorem prover or other suitable methods.