_______ __________  1   This work was supported by the EPSRC project EP/J011894/2.  Testing,   Verification   and Improvements of T imeliness in ROS  processes   1  Mohammed Y. Hazim, Hongyang Qu, and Sandor M. Veres  Dept. of Automatic Control and Systems   Engineering,   University of Sheffield , UK  {myhazim1,h.qu,s.veres}@shef.ac.uk  Abstract . This paper   addresses the problem   of   improving response times   of robots  implemented   in   the   Robotic   Operating   System   (ROS)   using   formal   verification   of  computational - time feasibility. In order to verify the real time behaviour of a robot under  uncertain signal processing times, methods of for mal verification of timeliness properties are  proposed for data flows in a ROS - based control system using Probabilistic Timed Programs  (PTPs). To calculate the probability of success under certain time limits, and to demonstrate  the strength of our approac h, a case study is implemented for a robotic agent in terms of  operational times verification using the PRISM model checker, which points to possible  enhancements to the operation of the robotic agent.  Keywords :   Verifi cation   _ ROS _ PTP _ LISA  1   Introduction  Th e Robot Operating Sy stem (ROS [10 ]) is an open - source operating system used to develop  control software for robots. It has become popular due to its capabilities in perception, object  detection,   navigation,   etc.   and   the   increasing   demand   for   a   uniform   platform   for  programmable robots. The correctness of a ROS program then attracts serious attention as  the deployment of ROS grows rapidly. An important way to guarantee correctness in software  is formal verification and several attempts have   been conducted to apply it to   ROS prog rams,  such as [9][4][11]. ROSRV in [ 4 ] is a runtime verification framework on top of ROS in order to  address safety and security   i ssues of robots. The work in [9 ] considered the problem of  generating a platform - specifi c glue code for platform - independent controller code in ROS,  and the code generation process is amenable to   formal verification. In [11 ], formal verification  was applied to a high - level planner/scheduler for autonomous personal robotic assistants  (Care - O - b ot). However, none of the attempts addresses the performance alongside the  correctness of a ROS program via formal verification to ensure stringent constraints on  timeliness and other properties in ROS programs. This assurance is crucial to correct system  behaviour and uncertainty in their environment.  This work is concerned with methods which can improve the performance of ROS based robot  control systems. One of the difficulties in robot programming is to ensure that the robot  responds to environmental cha llenges in a timely manner, let it be a threat approaching, to  avoid something or the execution of a command which should not be delayed. Physical
2  actions make the robot primarily depend on suitable speed of sensor signal processing, e.g.,  recognition   and   interpretation   of   relationships   of   static   and   moving   objects   in   the  environment, making sense of a command issued by a trusted human based on the context  the robot and the human share, or planning of an action sequence to achieve a goal in a timely  manner   which does not render the goal outdated by the time the plan is ready, etc.  The above computational challenges are addressed in the computational processes of ROS  while a number of nodes are running, each in possibly several threads that communicate with  e ach other between nodes. Broadcast of topics often interrupts subscriber nodes, and  services requested from other nodes need to be waited for in order to be able to make use  the data returned. For instance, sensing and recognition by computer vision may re quire  some fixed or variable time, depending on the significant number of objects of the  environment. Discovering relationships in the environment may however take even more  variable time to compute. Clearly action taking can suffer delays as planning cann ot start  before   relationships   are   modelled.   We   propose   that   improvements   to   ROS - based  computational performance can be analysed and carried out in three phases:  1.   Statistical modelling of computational times in various categories and complexities of  percep tion (including sensing and analysis), planning and execution of planned  actions.  2.   Formal analysis of the statistically modelled given ROS system using probab ilistic  timed programs (PTPs) [ 2 ] by answering PCTL queries on unacceptable delays in  computation   in oper ations by model checker PR ISM [ 7 ].  3.   Revision of procedures used in the ROS system to reduce the chance of computational  delays.  In this work, we first design a ROS system in a rational agent framework LISA (Limited  Instruction Set Architecture) [5 ] , which is based on AgentSpeak expansions such as Jason and  Jade, with more focusing on external planning process, abstraction from planning and  optimisation from decision making. The LISA model is then compiled into a PTP model for the  formal analysis.  2   The Robot Operating System  ROS is not a traditional Operating System. Rather it provides a structured communications  layer in which indiv idual processes can interact [10 ]. It simplifies the task of programming  robots by providing a robust framework where   the designer is provided a declarative  programming   environment   for   parallel   computational   processes   of   a   robot.   A   ROS  implementation of a robotic software has three typical components:     Nodes   -   Nodes are basic processes that perform the sensing, computation and control  tasks. Typically, each node can contain several computational threads, although it may
3  have additional sub - threads which the programmer is responsible for designing.  Typica l systems are formed from many nodes, each of which does a portion of the  overall task.     Services   -   Services provide a strict communication model where there is an established  request and response message between two nodes. In a process similar to web  servi ces, a node may subscribe and subsequently request in -   formation via a service  and then be supplied back with the information on demand.     Topics   -   In order to publish messages any node can establish a topic and publish  messages to it, as and when necessary.   Any other node within the network may also  publish to this topic. In order to receive messages, the other nodes may subscribe,  wherein they can receive any message sent via a call back. A topic is a broadcast  messaging stream and so does not provide any s ynchronous message transfer.  A fundamental difference between services and topics is that services are re -   quester/receiver  initiated while topics are sender/provider initiated and the receivers are immediately  notified, asynchronously. Both are however m any - to - many communications as there can be  several providers and receivers of any service or topic. Topics are inefficient when a node only  needs some data from another node occasionally, when it needs it; while services are  inefficient when a node needs s ome data supplied on a continuous, "as soon as possible"  basis, though asynchronously. In their own way both are efficient ways to communicate for  different purposes. Care needs to be taken however that a subscriber to a topic does not  receive more data th an it needs as otherwise it is wasting its computational resources on  handling redundant messages from the topic. For instance, sensor messages are to be  published to a topic only with a frequency which is needed by other nodes, thereby resulting  in less l atency than if a service were doing the same job.  3 Mathematical model of a ROS Package  One way to describe a ROS based system is a tri - partite graph with vertices for nodes, topics  and services. These vertex types are not interchangeable in graph matchi ng algorithms. New  topics and services can be easily introduced that can allow reconfiguration of the system to  provide agents with the information they required, albeit sourced from different locations.  All node communication must occur through topics or   services.  Definition 3.1. A ROS - graph is   𝐺   =   ( 𝑁 ,   𝑇 ,   𝑆 ,   𝐸 ,   𝐷 ,   𝐶 ,   𝑋 ,   𝜆 ) ,   where   𝑁   are the set of vertices  representing ROS nodes,   𝑇   are a set of topics and   𝑆   are a set of services,   𝐶   is a partially order  set of object classes and   𝑋   is a set of label s to name all vertices.   𝐸   ⊂   ( 𝑁   ×   𝑇 )   ∪   ( 𝑇   ×   𝑁 )   ∪  ( 𝑁   ×   𝑆 )   ∪   ( 𝑆   ×   𝑁 ) ,   is a set of directed edges to represent publishing of, and subscription to,  topics and provision of, and subscription to, services, respectively.   𝐷   ∶   𝐸 −   →   𝐶 ∗ ,   𝐸 −   =   𝑇   ∪  ( 𝑁   ×   𝑆 )   ∪   ( 𝑆   ×   𝑁 ) ,   is a data descriptor function where   𝐶 ∗   is a notation for finite sequences  of entries from the set of data object classes   𝐶 , which are used in services and topics to send
4  information between nodes. Each of   𝑁 ,   𝑇 ,   𝑆   are labelled by a surjective labellin g function  𝜆 :   𝑁   ∪   𝑇   ∪   𝑆   →   𝑋 .  A ROS system enables the nodes to advertise or use services, and to publish or subscribe to  topics. G represents the maximum ability of the robot when the system has all nodes, topics  and services nominally functioning. If some n odes are not available due to sensor, actuator  or computational hardware breakdown, then G needs sufficient redundancy to enable  continued functioning of the robot or at least some of its functionality. The ROS graph G  defines all the possible data flows f or sensor readings, signal processing and control action in  the environment. A detailed description is not within the scope of this work and we refer the  reader to [1].  4 Statistics of ROS nodes  When ROS based robot control system's programming is compl eted, the robot is ready to be  tested in a series of scenario tests. Performance may not acceptable due to a few factors:  1. When a plan of an agent is triggered due to environmental change the computational times  of perception modelling and planning ar e excessive and delay action taking in some  environmental scenarios.  2. In some environmental scenarios scene interpretation and planning is several times faster  than typical response time requires. The question arises whether more complex model of the  scene could have been built to more fully grasp an environmental situat ion.  Overall the performance problem of the robot is to discover scenarios which are not  favourable for the robot’s computational system. These are searched and synthesised based  on sensor and perception statistics derived in practical use of the ROS syst em. This section  provides a formal model of statistical estimation of computation and communication times in  a given ROS system already operating on a hardware platform. Consequent application of  probabilistic model checking can guide us to introduce impro vements in the choice of  computational processes involved in reasoning.  4.1 Performance evaluator node  To estimate the processing and communication time across the ROS system and additional  runtime statistics node   Σ   can be introduced, which collects runtime data from all the robots  functional nodes. Each of the functional nodes   𝑖   has a data array   𝐷 𝑖   recording timed -  performance of services and topics in the node. Let denote   𝑠 𝑘   ∈   𝑆   a service in a ROS - graph  𝐺   =   ( 𝑁 ,   𝑇 ,   𝑆 ,   𝐸 ,   𝐷 ,   𝐶 ,   𝑋 ,   𝜆 ) . The following timed data are recorded about a service call.  1. When a request is to be made from node   𝑗   for service   𝑠 𝑘 , then a data entry   ( 𝑛 𝑗   →  req  𝑠 𝑘 ,   𝑡 𝑗   )  is added to   𝐷 𝑗   just before the service command is issued from node   𝑗   to node   𝑖   with time  stamp   𝑡 𝑗   in node   𝑗 .
5  2. Upon request, and before any execution of service actions, a data entry   ( 𝑛 𝑗   →  req  𝑠 𝑘 ,   𝑡 𝑖   )   is  added to   𝐷 𝑖   with time stamp   𝑡 𝑖   in node   𝑖 .  3. Upon completion of the computational processes or physical   controls performed, a data  entry   ( 𝑛 𝑗   →  ans  𝑠 𝑘 ,   𝑡 𝑖   )   is added to   𝐷 𝑖   with time stamp in node   𝑖 .  4.   Upon answer data received in node   𝑗   for service   𝑠 𝑘 , then a data entry   ( 𝑛 𝑗   →  ans  𝑠 𝑘 ,   𝑡 𝑗 )   is  added to   𝐷 𝑗   with time stamp   𝑡 𝑗   in node   𝑗 .  For topics recording of runtime data is slightly different:  1. When a topic is to be published by node   𝑗   for topic   𝑝 𝑘 , then a data entry   ( 𝑛 𝑗   →  pub  𝑝 𝑘 ,   𝑡 𝑗   )   is  added to   𝐷 𝑗   just before the topic boadcast is issued from node   𝑗   with time stamp   𝑡 𝑗   in   node  𝑗 .  2.   Upon receiving the broadcast, and before any execution of actions due to the topic  broadcast, a data entry   ( 𝑛 𝑗   →  rec  𝑝 𝑘 ,   𝑡 𝑖 )   is added to   𝐷 𝑖   with time stamp   𝑡 𝑖   in node   𝑖 .  3. Upon completion of the computational processes or physical   controls performed, a data  entry   ( 𝑛 𝑗   →  top  𝑠 𝑘 ,   𝑡 𝑖 )   is added to   𝐷 𝑖   with time stamp in node   𝑖 .  Note that there are other ways to collect statistics on execution   time and latency, such as in  [ 3 ], but our method suits our need better because it does not   depend on the header of  messages, which is not always available.  4.2 Estimation of operations  From each node   𝑖   the data containers   𝐷 𝑖   are sent to the runtime statistics node   Σ , which can  compute the following amongst others:     Probability   distribution   of   the   request   communication   times   𝑡 𝑖   −   𝑡 𝑗   from  ( 𝑛 𝑗   →  req  𝑠 𝑘 ,   𝑡 𝑗   )   and   ( 𝑛 𝑗   →  req  𝑠 𝑘 ,   𝑡 𝑖   ) .     Probability distribution of the service execution times   𝑡 𝑠𝑖   −   𝑡 𝑒𝑖   f from   ( 𝑛 𝑗   →  req  𝑠 𝑘 ,   𝑡 𝑠𝑖   )  and   ( 𝑛 𝑗   →  ans  𝑠 𝑘 ,   𝑡 𝑒𝑖 ) .     Probability distribution answer communications times   𝑡 𝑗   −   𝑡 𝑖   from   ( 𝑛 𝑗   →  ans  𝑠 𝑘 ,   𝑡 𝑗   )   and  ( 𝑛 𝑗   →  ans  𝑠 𝑘 ,   𝑡 𝑖 ) .     Probability   distribution   of   communication   broadcast   times   𝑡 𝑖   −   𝑡 𝑗   from   of  ( 𝑛 𝑗   →  pub  𝑝 𝑘 ,   𝑡 𝑗   )   and   ( 𝑛 𝑗   →  rec  𝑝 𝑘 ,   𝑡 𝑖 ) .
6     Probability distribut ion of topic interruption times   ,   𝑡 𝑠𝑖   −   𝑡 𝑒𝑖   from   ( 𝑛 𝑗   →  rec  𝑝 𝑘 ,   𝑡 𝑠𝑖 )   and  ( 𝑛 𝑗   →  top  𝑠 𝑘 ,   𝑡 𝑒𝑖 ) .  Performance tuning of a ROS based computational system is carried out iteratively through a  series of trial runs, during which the average runtime probabi lities (or conditional runtime  probabilities of the duration events are evaluated), followed by a ROS system. This is followed  by algorithmic adjustments made to the ROS system and the iteration continues by another  trial run. The series of iterations cons isting of (1) trial - run (2) compilation to PRISM model (3)  running of PCTL queries (4) algorithmic amendments are cyclically repeated on the ROS  system until satisfactory computational performance is achieved.  5 A rational agent framework LISA  Comparing   with Jason in terms of plan selection function, LISA [ 5 ] proved to enhance the  architecture with a runtime probabilistic model checking by predicting the outcomes of  applicable plan and selections. The LISA structure is simpler than its predecessors and c an  easily lend itself to design time and run - time verification. Now we give the detail about LISA.  By analogy to previous definitions [8,   12 ] of AgentSpeak - like architectures, we define our  agents as a   tuple: ) , , , , ( =   A L B    F R   , where:   } , , , { =   2 1   p n p p p    F   is the set of all predicates.   F  B   is the total set of belief predicates. The current belief base at time t   is defined  as B B t      . Beliefs that are added, deleted or modified can be either called   internal   or  external   depending on whether they are generated from an internal action, in which  case are referred to as "mental notes", or from an external input, in which case they  are called "percepts".   } , , { =   2 1   l n l l l L      is a set of logic - based implication rules.   } , , , { =   2 1        n     is the set of executable plans or   plans library .  Current applicable plans at time t   are part of the subset applicable plan    t   or  "desire set".   B a a a A   a n   \ } , , , { =   2 1   F     is a set of all available a ctions. Actions can be either  internal , when they modify the belief base or data in memory objects, or   external ,  when they are linked to external functions that operate in the environment.  AgentSpeak like languages, including LISA, can be fully defined an d implemented by specifying  initial beliefs and actions, and reasoning cycles:     Initial Beliefs . The initial beliefs and goals F B    0   are a set of literals that are  automatically copied into the   belief base t B   (that is the set of current beliefs) when  the agent mind is first run.
7     Initial Actions . The initial actions A A    0   are a set of actions that are executed when  the agent mind is first run. The actions are generally goals that activate spec ific plans.  The following operations are repeated for each reasoning cycle in AgentSpeak.     Maintenance of Percepts . This means generation of perception predicates for t B   and  data objects such as the world model used here W   .     Logic rules . A set of logic based implication rules L   describes   theoretical   reasoning to  improve the agent current knowledge about the world.     Executable plans . A set of   executable plans   or   plan library    . Each plan j     is  described in the form: j n j j   a a a c p   , , , :   2 1       , where B p   j      is a   triggering predicate ,  which allows the plan to be retrieved from the plan library whenever it comes true, B c   j     is a logic formula of a   context , which allows the agent to check the state of the  world, described by the current belief set t B   , before applying a particular plan  sequence A a a a   j n    , , ,   2 1      with a list of actions. Each j a   can be one of (1) predicate  of an external action with arguments of names of data objects, (2) internal (mental  note) with a preceding + or   -   sign to indicate whether the predicate needs to be added  or taken away from the belief set t B   (3) conditional set of items from (1) - (2). The set  of all triggers j p   in a program is denoted by tr E  LISA enhanced the above reasoning cycle to allow multiple actions to be executed in parallel.  The enhanced reasoning cycle consists of the following steps:  1.   Belief base update . The agent updates the belief base by retrieving information about  the world th rough perception and communication. Adding and removing beliefs from  the belief base is carried out by the function   Belief Update Function (BUF) .  2.   Application of logic rules . The logic rules in L   are applied in a round - robin fashion  (re starting at the beginning of the list) until there are no new predicates generated for t B  . This means that rules need to be verified not to lead to infinite loops.  3.   Trigger Event Selection . For every reasoning cycle a function called   Be lief Review  Function ) ( ) ( :   t t t   E B S        selects the current event set t E   , where ) (     is the so  called   power operator   and represents the set of all possible subset of a particular set.  We call the current selected t rigger event t t   T B S   = ) (   and the associated plans the  Intention Set .  4.   Plan Selection . All the plans in t T   are checked for their context to form the   Applicable  Plans   set t    by function ) ( :   t t O   S E S       . We will call the current selected plan t t O S   = ) (   .
8  5.   Plan Executions . All plans in t O   E S   :   are started to be executed concurrently by going  through the plan items j n a a a   , , ,   2 1      one - by - one sequentially.  6 Modelling of   agent operational times in PRISM  In this section we assume that the response of the physical environment of the agent is  modelled as a probabilistic timed program (PTP)   𝐸   in terms of the predicates feed back to the  belief base of the agent under various environmental states.   𝐸   is composed of environmental  states, and transitions which under each state through the conditional probabilities of the  environment corresponds to   triggering of predicates through the sensor system of the robotic  agent. Given that the agent has well defined decision structures as described in the previous  section, the environment - agent model will also be a PTP. This section describes how the  combina tion of probability distributions, which were estimated in the previous section, when  combined with the environmental PTP and the logic based decision making of the agent, can  be modelled in PRISM.  6.1 Probabilistic timed programs (PTP)  Probabilistic tim ed programs   [6 ] are an extension of Markov Decision Processes (MDPs) with  state variables and real - time clocks.  Given a set   𝒱   of variables, let   ( 𝒱 ) ,   𝑉𝑎𝑙 ( 𝒱 )   and   ( 𝒱 )   be a set of   assertions ,   valuations   and  assignments   over   𝒱   respectively. Given a set   𝑆 , let   𝑆   be the set of subsets of   𝑆   and   𝑆   the set  of discrete probability distributions over   𝑆 . A set   𝒳   of   clock   variables represents the time  elapsed since the occurrence of various events. The set of   clock valuations   is   ℝ ≥ 0  𝒳   =   { 𝑡 :   →  ℝ ≥ 0 } . For any clo ck valuation   𝑡   and any   𝛿   ≥   0 , the   delayed   valuation   𝑡   +   𝛿   is defined by   ( 𝑡   +  𝛿 ) ( 𝑥 )   =   𝑡 ( 𝑥 )   +   𝛿   for all   𝑥   ∈   𝒳 . For a subset   𝑌   ⊆   𝒳 , the valuation   𝑡 [ 𝑌 :   =   0 ]   is obtained by  setting all clocks in   𝑌   to   0 :   𝑡 [ 𝑌 :   =   0 ] ( 𝑥 )   is   0   if   𝑥   ∈   𝑌   and   𝑡 ( 𝑥 )   otherwise. A (convex)   zone   is  the set of clock valuations satisfying a number of clock difference constraints, i.e. a set of the  form:   𝜌   =   { 𝑡   ∈   ℝ ≥ 0  𝒳 0   |   𝑡 𝑖   −   𝑡 𝑗   ≲   𝑏 𝑖𝑗 } . The set of all zones is   𝑍𝑜𝑛𝑒𝑠 ( 𝒳 ) .  Definition 1 (PTP).   A PTP is a tuple   𝑃   =   ( 𝐿 ,   𝑙 0 ,   𝒳 ,   𝒱 ,   𝑣 𝑖 ,   ℐ ,   𝒯 )   where:     𝐿   is a finite set of   locations   and   𝑙 0   ∈   𝐿   is the   initial location ;     𝒳   is a finite set of   clocks   and   ℐ :   𝑆   →   𝑍𝑜𝑛𝑒𝑠 ( 𝒳 )   is the   invariant condition ;     𝒱   is a finite set of   state variables   and   𝑣 𝑖   ∈   𝑉𝑎𝑙 ( 𝒱 )   is the   initial   valuation ;     𝒯 :   𝑆   →   𝑇𝑟𝑎𝑛𝑠 ( 𝐿 ,   𝒱 ,   𝒳 )   is   the   probabilistic   transition   function ,   where  𝑇𝑟𝑎𝑛𝑠 ( 𝐿 ,   𝒱 ,   𝒳 )   =   Asrt ( 𝒱 )   ×   𝑍𝑜𝑛𝑒𝑠 ( 𝒳 )   ×   D ( Assn ( 𝒱 )   ×   P ( 𝒳 )   ×   𝐿 ) .  A step from a state   ( 𝑙 ,   𝑣 ,   𝑡 )   consists of the elapse of a certain amount of time   𝛿   ∈   ℝ ≥ 0  followed by a   transition   𝜏   =   ( 𝒢 ,   ℰ ,   Δ )   ∈   𝒯 ( 𝑙 ) . The transition comprises a   guard   𝒢   ∈   Asrt ( 𝒱 ) ,  enabling   condition   ℰ   ∈   𝑍𝑜𝑛𝑒𝑠 ( 𝒳 )   and   probability   distribution   Δ   =   𝜆 1 ( 𝑓 1 ,   𝑟 1 ,   𝑙 1 )   +   ⋯   +
9  𝜆 𝑘 ( 𝑓 𝑘 ,   𝑟 𝑘 ,   𝑙 𝑘 ) )   over triples containing an   update   𝑓 𝑗   ∈   Asrt ( 𝒱 ) , clock   resets   𝑟 𝑗   ⊆   𝒳   and   target  location   𝑙 𝑗   ∈   𝐿 .  The delay   𝛿   must be chosen such that the invariant   ℐ ( 𝑙 )   remains continuously satisfied; since  ℐ ( 𝑙 )   is a (convex) zone, this is equivalent to requiring that both   𝑡   and   𝑡   +   𝛿   satisfy   ℐ ( 𝑙 ) . The  chosen transition   𝜏   must be   enabled , i.e., the guard   𝒢   and the enabling condition   ℰ   in   𝜏   must  be satisfied by   𝑣   and   𝑡   +   𝛿 , respectively. Once   𝜏   is chosen, an assignment, set of clocks to  reset, and successor location are selected at random, according to the distribution   Δ   in   𝜏 .  6.2 Performance queries  Given a PTP, we can use the following PCTL queries to check its properties:  •   P ⋈ = ? [ F   𝑎 ] ,  •   P ⋈ = ? [ F ≤ 𝑇   𝑎 ] ,  where   ⋈ ∈   { 𝑚𝑎𝑥 ,   𝑚𝑖𝑛 } ,   𝑎   is Boolean expression that does not refer to any clocks and   𝑇   is an  integer expression. The first query asks what is the maximum/minimum probability that   𝑎   is  satisfied, and the second one inquires the probability that   𝑎   can be satisfied within time  bound   𝑇 . Based on these queries, we can compute the maximum/mini mum probability of all  target states that satisfy   𝑎   without time limit or within a bound   𝑇 . For example, we can ask  what is the minimum probability for a robot moving to a specific location within certain time.  A concrete example will be shown in the nex t section.  6.3 Verification process  Figure 1 illustrates the whole process in our method. A system is first written in LISA and then  translated into ROS. A performance evaluator node is generated for this system. After the  evaluator node collects suffici ent statistics on the time delay, it computes the probability  distribution. A PTP model is then constructed using this information and the LISA program,  although it is feasible to build the PTP model from the ROS program directly. The reason that  we build   the PTP model from the LISA program is that it provides a high level abstraction of  the system, which can make the PTP model compact. The PTP model is fed to PRISM for  verification. The result is then used as a reference when improving the design of the RO S  program.
10  Figure 1: The verification process .  7   Case study  In this section we demonstrate the strength of our approach using the following scenario. An  autonomous ground vehicle (AGV) is exploring a remote area with a vision system consisting  two cameras (primary and secondary camera). The system merges two images , one from each  camera, to look for an object in the area. Here we are mainly interested in two ROS nodes:  one for receiving images from the cameras and the other for processing these images. The  statistics shows that time   for receiving one image   respect t he following probability  distribution:  • With probability   0 . 3 , it take less than 4 units of time, but more than 3 units to receive one  image;  • With probability   0 . 6 , the receiving time locates in the interval   ( 4 , 6 ) ;  • With probability   0 . 1 , the receivin g time locates in   ( 6 , 8 ) .  It takes less than 16 units of time but more than 12 units to process two images, and the  probability of successfully finding the object in the images is 0.91. When the system fails to  find the object, it will take two new images   from the cameras and repeat the process.  Fig ure   2 : The PTP for the system .
11  Figure   2   illustrates the PTP model for the system, where   𝑥   is a clock, which is used to count  the time elapse for each step. The timing constraints in a node (which represents a state),  such as   𝑥   <   4 , is the upper bound and the constraints on an edge (which represents a  transition), such as   𝑥   >   3 , is the lower boun d. This figure shows that the system receives the  image from the primary camera first (states   𝑠 1 ,   𝑠 2   and   𝑠 3 ), and then receives the one from  the secondary camera (states   𝑠 4 ,   𝑠 5   and   𝑠 6 ). In state   𝑠 7 , the system processes the images. We  can ask a quer y that at what probability the system successfully find the object within 35 units  of time, which can formulated in PCTL as follows:  P 𝑚𝑎𝑥 = ? [ F ≤ 35   `` 𝑆𝑢𝑐𝑐𝑒𝑠𝑠 ′′   ]   (1)  Figure   3 : The PTP for   the new system .  The result returned by PRISM is   0 . 91 . One problem in this system is that it has to wait for two  images before it can start to look for the object. If the image processing and receiving can be  performed in parallel by different hardware, we   may be able to increase the performance of  the system, which is possible if the object can be found from one image, even if at a lower  probability, e.g., 0.7. One way to achieve it as follows. The system starts to process the first  image immediately after   it arrives. Here we assume that processing one image is between 8  and 10 units. As the processing time exceeds the time required for receiving an image, the  system does not need to wait once it finishes processing the first image. Instead, it can  immediat ely process the second images. Although it is slightly slower to process the images  separately than processing them altogether, eliminating the waiting time for the second  image makes the system able to receive more images within the time limit and thus, f ind the  object at higher probability. Figure   3   illustrates the improved system design. The result for  the query in Equation (1) is   0 . 9724 , which shows a big improvement fr om the previous design.  Figure   4   shows the PRISM program for this improved system.
12  Fig ure   4 : The Prism program for the new system.  8 Conclusions  This paper pre sented a method for formal verifi cat ion of timeliness properties of   robots  implemented in ROS. The LISA framework was used to design a rob otic   agent as LISA p rovides  a solution   for the verifi c ation of robotic agents through   the PRISM model checker. Statistical  estimation   was applied to robot operations   under the ROS system to detect and collect  i nformation about the latency in   the system. The LISA model was then associated   with  r untime probabilities and   trans lated into a PTP model and verifi ed in PRI SM. It has been  illustrated how   to apply the methods to improve the design of a ROS system in a case study.  In the future we intend to bring the method s nearer to industrial applica bil ity by improving  their timing performance an alysis, which might require the development of more eff icient  model checking   algorithms for PTPs in the case   of very large models. Another direction of  future work is to searc h for other   modelling formalisms, whi ch can handle continuo us  probability distributions on   timing variances, as PTP can only deal with discrete probability  distributions.  References  1. J. M Aitken, S. M. Veres, and M. Judge. Adaptati on of system confi guration under the robot  operating   system. In Proc. of the 19th world congress of the international federation of  automatic control, 2014.  2. K. Dr ager, M. Z. Kwiatkowska, D. Parker, and   H. Qu. Local abstraction refinement   for  probabilistic timed programs. Theor. Comput. Sci., 538:37 - 53,   2014.  3. D. Forouher, J. Hartmann, and E. Maehle. Data ow analysis in ROS. In   Proc. Of   the 41st  International Symposium on Robotics, pages 1{6. VDE, 2014.  4. J. Huang, C. Erdogan, Y. Zhang, B. Moore, Q. L uo, A. Sundaresan, and G. Rosu. ROSRV:  Runtime verif i cation for robots. In Proc.   of the 14th International Conference on Runtime  Verifi cation, LNCS 8734, pages 247{254. Springer, 2014.
13  5. P. Izzo, H. Qu, and S. M. Veres. Reducing c omplexity of autonomous control agents for  verifi ability. arXiv:1603.01202[cs .SY], March 2016.  6. M. Kwiatkowska, G. Norman, and D. Parker.   A framework for verification of   software with  time and probabilities. In Proc. of t he 8th International Conference   on Formal Modelling and  Analysis of Timed Systems , LNCS 6246, pages 25 - 45.   Spr inger, 2010.  7. M. Kwiatkowska, G. Norman, and D. Parker. Prism 4. 0: Verification of probabilistic   real - time  systems. In Computer aided v erifi cation, pages 585{591. Springer, 2011.  8. N. K. Lincoln and S. M. Veres. Natural language   programming of complex r obotic   BDI agents.  Intelligent and Robotic Systems, 71(2):211 - 230, 2013.  9. W. Meng, J. Park, O. Sokolsk y, S. Weirich, and I. Lee. Verifi ed   ROS - based deployment   of  platform - independent control systems. In Proc. of NASA Formal Methods , LNCS 9058, pages  248 - 262. Springer, 2015.  10. M. Quigley, K. Conley, B. P. Gerkey, J. Faust, T. F oote, J. Leibs, R. Wheeler, and   A. Y. Ng.  ROS: an open - source Robot Operating System. In   ICRA Workshop on   Open Source Software,  volume 3, 2009.  11. M. Webster, C. Dixon, M. Fisher,   M. Salem, J. Saunde rs, K. Koay, and K. Dautenhahn.  Formal verifi cation of an autonomous personal robotic assistant , pages   74{79. AAAI, 2014.  12. M. Wooldridge. An Introduction to MultiAgent Systems. Wiley, Chichester, 2002.